case h.e'_3.h.e'_3
α : Type u_1
β : Type ?u.18650
R : Type ?u.18653
R' : Type ?u.18656
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
t s : Set α
⊢ t = t ∩ s ∪ t \ s
α : Type u_1
β : Type ?u.18650
R : Type ?u.18653
R' : Type ?u.18656
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
t s : Set α
⊢ ↑m t ≤ ↑m (t ∩ s) + ↑m (t \ s)
convert m.union _ _
no goals
case h.e'_3.h.e'_3
α : Type u_1
β : Type ?u.18650
R : Type ?u.18653
R' : Type ?u.18656
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
t s : Set α
⊢ t = t ∩ s ∪ t \ s
rw [inter_union_diff t s]