Theorem: MeasureTheory.measureReal_union₀ (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 α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∪ t) = μ.real s + μ.real t
Tactic:
simp only [Measure.real]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∪ t)).toReal = (μ s).toReal + (μ t).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ (μ (s ∪ t)).toReal = (μ s).toReal + (μ t).toReal
Tactic:
rw [measure_union₀ ht hd, ENNReal.toReal_add h₁ h₂]
State after:
no goals