no goals
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : IsCaratheodory m s₁
t : Set α
⊢ ↑m (t ∩ (s₁ ∪ s₂)) = ↑m (t ∩ s₁) + ↑m (t ∩ s₂)
rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]