Theorem: MeasureTheory.measureReal_eq_measureReal_of_between_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₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃
Tactic:
have A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃ :=
  measure_eq_measure_of_between_null_diff h12 h23 ((measureReal_eq_zero_iff h').1 h_nulldiff)
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁✝ s₂✝ t s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : autoParam (μ (s₃ \ s₁) ≠ ⊤) _auto✝
A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃

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