α : Type u_1
β : Type ?u.20498
R : Type ?u.20501
R' : Type ?u.20504
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s t : Set α
ht : ↑m t = 0
⊢ ↑m s ≤ ↑m (s \ t)
α : Type u_1
β : Type ?u.20498
R : Type ?u.20501
R' : Type ?u.20504
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s t : Set α
ht : ↑m t = 0
⊢ ↑m (s \ t) = ↑m s
refine' le_antisymm (m.mono <| diff_subset _ _) _
no goals
α : Type u_1
β : Type ?u.20498
R : Type ?u.20501
R' : Type ?u.20504
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s t : Set α
ht : ↑m t = 0
⊢ ↑m s ≤ ↑m (s \ t)
calc
  m s ≤ m (s ∩ t) + m (s \ t) := le_inter_add_diff _
  _ ≤ m t + m (s \ t) := (add_le_add_right (m.mono <| inter_subset_right _ _) _)
  _ = m (s \ t) := by rw [ht, zero_add]
no goals
α : Type u_1
β : Type ?u.20498
R : Type ?u.20501
R' : Type ?u.20504
ms : Set (OuterMeasure α)
m✝ m : OuterMeasure α
s t : Set α
ht : ↑m t = 0
⊢ ↑m t + ↑m (s \ t) = ↑m (s \ t)
rw [ht, zero_add]