Theorem: MeasureTheory.measureReal_diff_null (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 : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Tactic:
rcases eq_top_or_lt_top (μ s₁) with H|H
State after:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ = ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁

case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ < ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁

State before:
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ = ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Tactic:
simp [measureReal_def, H, measure_diff_eq_top H h']
State after:
no goals

State before:
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : μ.real s₂ = 0
h' : autoParam (μ s₂ ≠ ⊤) _auto✝
H : μ s₁ < ⊤
⊢ μ.real (s₁ \ s₂) = μ.real s₁
Tactic:
exact measureReal_diff_null' (measureReal_mono_null inter_subset_right h h') H.ne
State after:
no goals