α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ↑(trim m) s
simp only [trim_eq_iInf]
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
set ms := ⨅ (t : Set α) (st : s ⊆ t) (ht : MeasurableSet t), m t
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms

case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
by_cases hs : ms = ∞
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ⊤
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
simp only [hs]
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ∀ (i : Set α), s ⊆ i → MeasurableSet i → ↑m i = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ⊤
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ⊤
simp only [iInf_eq_top] at hs
no goals
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ∀ (i : Set α), s ⊆ i → MeasurableSet i → ↑m i = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ⊤
exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
have : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r := by
  intro r hs
  have : ∃t, MeasurableSet t ∧ s ⊆ t ∧ measureOf m t < r := by simpa [iInf_lt_iff] using hs
  rcases this with ⟨t, hmt, hin, hlt⟩
  exists t
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
this : ∀ (n : ℕ), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < ms + (↑n)⁻¹
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
have : ∀ n : ℕ, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (n : ℝ≥0∞)⁻¹ := by
  intro n
  refine' this _ (ENNReal.lt_add_right hs _)
  simp
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
this : ∀ (n : ℕ), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < ms + (↑n)⁻¹
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
choose t hsub hm hm' using this
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
⊢ ↑m (⋂ (n : ℕ), t n) = ms
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ms
refine' ⟨⋂ n, t n, subset_iInter hsub, MeasurableSet.iInter hm, _⟩
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 (ms + 0))
⊢ ↑m (⋂ (n : ℕ), t n) = ms
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
⊢ ↑m (⋂ (n : ℕ), t n) = ms
have : Tendsto (fun n : ℕ => ms + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0)) :=
  tendsto_const_nhds.add ENNReal.tendsto_inv_nat_nhds_zero
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ↑m (⋂ (n : ℕ), t n) = ms
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 (ms + 0))
⊢ ↑m (⋂ (n : ℕ), t n) = ms
rw [add_zero] at this
case neg.refine'_1
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
n : ℕ
⊢ ↑m (⋂ (n : ℕ), t n) ≤ ms + (↑n)⁻¹

case neg.refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ms ≤ ↑m (⋂ (n : ℕ), t n)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ↑m (⋂ (n : ℕ), t n) = ms
refine' le_antisymm (ge_of_tendsto' this fun n => _) _
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
⊢ ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
intro r hs
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
this : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ ↑m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
have : ∃t, MeasurableSet t ∧ s ⊆ t ∧ measureOf m t < r := by simpa [iInf_lt_iff] using hs
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
t : Set α
hmt : MeasurableSet t
hin : s ⊆ t
hlt : ↑m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
this : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ ↑m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
rcases this with ⟨t, hmt, hin, hlt⟩
no goals
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
t : Set α
hmt : MeasurableSet t
hin : s ⊆ t
hlt : ↑m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
exists t
no goals
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, MeasurableSet t ∧ s ⊆ t ∧ ↑m t < r
simpa [iInf_lt_iff] using hs
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
n : ℕ
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < ms + (↑n)⁻¹
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
⊢ ∀ (n : ℕ), ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < ms + (↑n)⁻¹
intro n
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
n : ℕ
⊢ (↑n)⁻¹ ≠ 0
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
n : ℕ
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < ms + (↑n)⁻¹
refine' this _ (ENNReal.lt_add_right hs _)
no goals
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
n : ℕ
⊢ (↑n)⁻¹ ≠ 0
simp
no goals
case neg.refine'_1
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
n : ℕ
⊢ ↑m (⋂ (n : ℕ), t n) ≤ ms + (↑n)⁻¹
exact le_trans (m.mono' <| iInter_subset t n) (hm' n).le
case neg.refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ (⨅ (_ : s ⊆ ⋂ (n : ℕ), t n) (_ : MeasurableSet (⋂ (n : ℕ), t n)), ↑m (⋂ (n : ℕ), t n)) ≤ ↑m (⋂ (n : ℕ), t n)
case neg.refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ ms ≤ ↑m (⋂ (n : ℕ), t n)
refine' iInf_le_of_le (⋂ n, t n) _
case neg.refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ (⨅ (_ : MeasurableSet (⋂ (n : ℕ), t n)), ↑m (⋂ (n : ℕ), t n)) ≤ ↑m (⋂ (n : ℕ), t n)
case neg.refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ (⨅ (_ : s ⊆ ⋂ (n : ℕ), t n) (_ : MeasurableSet (⋂ (n : ℕ), t n)), ↑m (⋂ (n : ℕ), t n)) ≤ ↑m (⋂ (n : ℕ), t n)
refine' iInf_le_of_le (subset_iInter hsub) _
no goals
case neg.refine'_2
α : Type u_1
inst✝ : MeasurableSpace α
m✝ m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
hs : ¬ms = ⊤
this✝ : ∀ (r : ℝ≥0∞), r > ms → ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), ↑m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n => ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ (⨅ (_ : MeasurableSet (⋂ (n : ℕ), t n)), ↑m (⋂ (n : ℕ), t n)) ≤ ↑m (⋂ (n : ℕ), t n)
refine' iInf_le _ (MeasurableSet.iInter hm)