Theorem: MeasureTheory.measureReal_add_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✝ : Set α
hs : MeasurableSet s
t : Set α
h₁ : autoParam (μ s ≠ ⊤) _auto✝
h₂ : autoParam (μ t ≠ ⊤) _auto✝
⊢ μ.real s + μ.real (t \ s) = μ.real (s ∪ t)
Tactic:
rw [← measureReal_union' (@disjoint_sdiff_right _ s t) hs h₁
  (measure_ne_top_of_subset diff_subset h₂), union_diff_self]
State after:
no goals