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

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