Theorem: MeasureTheory.measureReal_mono_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 : s₁ ⊆ s₂
h₂ : μ.real s₂ = 0
h'₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ = 0
Tactic:
rw [measureReal_eq_zero_iff h'₂] at h₂
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
h : s₁ ⊆ s₂
h₂ : μ s₂ = 0
h'₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ = 0

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₂ : μ s₂ = 0
h'₂ : autoParam (μ s₂ ≠ ⊤) _auto✝
⊢ μ.real s₁ = 0
Tactic:
simp [Measure.real, measure_mono_null h h₂]
State after:
no goals