α : Type u_1
β : Type ?u.5141
γ : Type ?u.5144
δ : Type ?u.5147
ι : Type ?u.5150
R : Type ?u.5153
R' : Type ?u.5156
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
⊢ ↑↑μ t + ↑↑μ (s \ t) + ↑↑μ (s ∩ t) = ↑↑μ (s ∩ t) + ↑↑μ (s \ t) + ↑↑μ t
α : Type u_1
β : Type ?u.5141
γ : Type ?u.5144
δ : Type ?u.5147
ι : Type ?u.5150
R : Type ?u.5153
R' : Type ?u.5156
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
⊢ ↑↑μ (s ∪ t) + ↑↑μ (s ∩ t) = ↑↑μ s + ↑↑μ t
rw [← measure_inter_add_diff (s ∪ t) ht, Set.union_inter_cancel_right, union_diff_right, ←
  measure_inter_add_diff s ht]
no goals
α : Type u_1
β : Type ?u.5141
γ : Type ?u.5144
δ : Type ?u.5147
ι : Type ?u.5150
R : Type ?u.5153
R' : Type ?u.5156
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
ht : MeasurableSet t
⊢ ↑↑μ t + ↑↑μ (s \ t) + ↑↑μ (s ∩ t) = ↑↑μ (s ∩ t) + ↑↑μ (s \ t) + ↑↑μ t
ac_rfl