no goals
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
x✝ : MeasurableSet s
t : Set α
hs₁ : s ∈ (fun m => {t | MeasurableSet t}) (OuterMeasure.caratheodory m₁)
hs₂ : s ∈ (fun m => {t | MeasurableSet t}) (OuterMeasure.caratheodory m₂)
⊢ ↑(m₁ + m₂) t = ↑(m₁ + m₂) (t ∩ s) + ↑(m₁ + m₂) (t \ s)
simp [hs₁ t, hs₂ t, add_left_comm, add_assoc]