Theorem: MeasureTheory.measureReal_diff (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : s₂ ⊆ s₁
h₂ : MeasurableSet s₂
h₁ : autoParam (μ s₁ ≠ ⊤) _auto✝
⊢ μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂
Tactic:
rw [measureReal_diff' _ h₂ h₁ (measure_ne_top_of_subset h h₁), union_eq_self_of_subset_right h]
State after:
no goals