Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ (sᶜ) ≠ 0
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t ∩ sᶜ) = ↑↑μ t
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ (sᶜ) ≠ 0
⊢ ↑↑(μ[|s]) t * ↑↑μ s + ↑↑(μ[|sᶜ]) t * ↑↑μ (sᶜ) = ↑↑μ t
rw [cond_mul_eq_inter μ hms hcs, cond_mul_eq_inter μ hms.compl hcs', Set.inter_comm _ t,
  Set.inter_comm _ t]
no goals
Ω : Type u_1
m : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
s t : Set Ω
inst✝ : IsFiniteMeasure μ
hms : MeasurableSet s
hcs : ↑↑μ s ≠ 0
hcs' : ↑↑μ (sᶜ) ≠ 0
⊢ ↑↑μ (t ∩ s) + ↑↑μ (t ∩ sᶜ) = ↑↑μ t
exact measure_inter_add_diff t hms