α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
h₁ : IsCaratheodory m s₁
h₂ : IsCaratheodory m s₂
t : Set α
⊢ ↑m (t ∩ s₁ ∩ s₂) + ↑m ((t ∩ s₁) \ s₂) + (↑m (t \ s₁ ∩ s₂) + ↑m ((t \ s₁) \ s₂)) =
    ↑m (t ∩ s₁ ∩ s₂) + ↑m ((t ∩ s₁) \ s₂) + ↑m (t ∩ (s₂ \ s₁)) + ↑m (t \ (s₁ ∪ s₂))
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
h₁ : IsCaratheodory m s₁
h₂ : IsCaratheodory m s₂
t : Set α
⊢ ↑m t = ↑m (t ∩ (s₁ ∪ s₂)) + ↑m (t \ (s₁ ∪ s₂))
rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)), inter_diff_assoc _ _ s₁,
  Set.inter_assoc _ _ s₁, inter_eq_self_of_subset_right (Set.subset_union_left _ _),
  union_diff_left, h₂ (t ∩ s₁)]
no goals
α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
h₁ : IsCaratheodory m s₁
h₂ : IsCaratheodory m s₂
t : Set α
⊢ ↑m (t ∩ s₁ ∩ s₂) + ↑m ((t ∩ s₁) \ s₂) + (↑m (t \ s₁ ∩ s₂) + ↑m ((t \ s₁) \ s₂)) =
    ↑m (t ∩ s₁ ∩ s₂) + ↑m ((t ∩ s₁) \ s₂) + ↑m (t ∩ (s₂ \ s₁)) + ↑m (t \ (s₁ ∪ s₂))
simp [diff_eq, add_assoc]