α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hst : ∀ (i : ι), s ⊆ t i
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(trim (μ i)) s
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(trim (μ i)) s
choose t hst ht hμt using fun i => (μ i).exists_measurable_superset_eq_trim s
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(trim (μ i)) s
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hst : ∀ (i : ι), s ⊆ t i
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(trim (μ i)) s
replace hst := subset_iInter  hst
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet (⋂ (b : ι), t b)
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(trim (μ i)) s
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
ht : ∀ (i : ι), MeasurableSet (t i)
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(trim (μ i)) s
replace ht := MeasurableSet.iInter ht
case refine'_1
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet (⋂ (b : ι), t b)
i : ι
⊢ ↑(μ i) (⋂ (i : ι), t i) ≤ ↑(trim (μ i)) s

case refine'_2
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet (⋂ (b : ι), t b)
i : ι
⊢ ↑(trim (μ i)) s ≤ ↑(μ i) (⋂ (i : ι), t i)
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet (⋂ (b : ι), t b)
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(trim (μ i)) s
refine' ⟨⋂ i, t i, hst, ht, fun i => le_antisymm _ _⟩
no goals
case refine'_1
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet (⋂ (b : ι), t b)
i : ι
⊢ ↑(μ i) (⋂ (i : ι), t i) ≤ ↑(trim (μ i)) s

case refine'_2
α : Type u_2
inst✝¹ : MeasurableSpace α
m : OuterMeasure α
ι : Sort u_1
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), ↑(μ i) (t i) = ↑(trim (μ i)) s
hst : s ⊆ ⋂ (i : ι), t i
ht : MeasurableSet (⋂ (b : ι), t b)
i : ι
⊢ ↑(trim (μ i)) s ≤ ↑(μ i) (⋂ (i : ι), t i)
exacts [hμt i ▸ (μ i).mono (iInter_subset _ _), (mono' _ hst).trans_eq ((μ i).trim_eq ht)]