α : Type u_1
β : Type ?u.84556
γ : Type ?u.84559
δ : Type ?u.84562
ι : Type ?u.84565
R : Type ?u.84568
R' : Type ?u.84571
ms : MeasurableSpace α
s✝ t : Set α
m : OuterMeasure α
h : ms ≤ OuterMeasure.caratheodory m
s : Set α
hs : NullMeasurableSet s
⊢ ↑↑(OuterMeasure.toMeasure m h) s ≤ ↑m s
α : Type u_1
β : Type ?u.84556
γ : Type ?u.84559
δ : Type ?u.84562
ι : Type ?u.84565
R : Type ?u.84568
R' : Type ?u.84571
ms : MeasurableSpace α
s✝ t : Set α
m : OuterMeasure α
h : ms ≤ OuterMeasure.caratheodory m
s : Set α
hs : NullMeasurableSet s
⊢ ↑↑(OuterMeasure.toMeasure m h) s = ↑m s
refine' le_antisymm _ (le_toMeasure_apply _ _ _)
case intro.intro.intro
α : Type u_1
β : Type ?u.84556
γ : Type ?u.84559
δ : Type ?u.84562
ι : Type ?u.84565
R : Type ?u.84568
R' : Type ?u.84571
ms : MeasurableSpace α
s✝ t✝ : Set α
m : OuterMeasure α
h : ms ≤ OuterMeasure.caratheodory m
s : Set α
hs : NullMeasurableSet s
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᵐ[OuterMeasure.toMeasure m h] s
⊢ ↑↑(OuterMeasure.toMeasure m h) s ≤ ↑m s
α : Type u_1
β : Type ?u.84556
γ : Type ?u.84559
δ : Type ?u.84562
ι : Type ?u.84565
R : Type ?u.84568
R' : Type ?u.84571
ms : MeasurableSpace α
s✝ t : Set α
m : OuterMeasure α
h : ms ≤ OuterMeasure.caratheodory m
s : Set α
hs : NullMeasurableSet s
⊢ ↑↑(OuterMeasure.toMeasure m h) s ≤ ↑m s
rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, heq⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.84556
γ : Type ?u.84559
δ : Type ?u.84562
ι : Type ?u.84565
R : Type ?u.84568
R' : Type ?u.84571
ms : MeasurableSpace α
s✝ t✝ : Set α
m : OuterMeasure α
h : ms ≤ OuterMeasure.caratheodory m
s : Set α
hs : NullMeasurableSet s
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᵐ[OuterMeasure.toMeasure m h] s
⊢ ↑↑(OuterMeasure.toMeasure m h) s ≤ ↑m s
calc
  m.toMeasure h s = m.toMeasure h t := measure_congr heq.symm
  _ = m t := (toMeasure_apply m h htm)
  _ ≤ m s := m.mono hts