Theorem: MeasureTheory.measureReal_union_add_inter₀ (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 : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Tactic:
have : μ (s ∪ t) ≠ ∞ :=
  ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨h₁.lt_top, h₂.lt_top⟩ )).ne
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.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 : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Tactic:
rw [← measureReal_inter_add_diff₀ (s ∪ t) ht this, Set.union_inter_cancel_right, union_diff_right,
  ← measureReal_inter_add_diff₀ s ht h₁]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t s : Set α
ht : NullMeasurableSet t μ
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
this : μ (s ∪ t) ≠ ⊤
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t
Tactic:
ac_rfl
State after:
no goals