-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem exists_measurable_superset_eq_trim (m : OuterMeasure α) (s : Set α) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this : ∀ 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

Tactic:
have : Tendsto (fun n : ℕ => ms + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0)) :=
  tendsto_const_nhds.add ENNReal.tendsto_inv_nat_nhds_zero

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this✝ : ∀ 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

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = m.trim s

Tactic:
simp only [trim_eq_iInf]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
n : ℕ
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (↑n)⁻¹

Tactic:
refine this _ (ENNReal.lt_add_right hs ?_)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
n : ℕ
⊢ (↑n)⁻¹ ≠ 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
by_cases hs : ms = ∞

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
⊢ ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Tactic:
intro r hs

Result:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ∀ (i : Set α), s ⊆ i → MeasurableSet i → m i = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ⊤

Tactic:
exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this✝ : ∀ 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

Tactic:
choose t hsub hm hm' using this

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this : ∀ 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

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : 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

Tactic:
rcases this with ⟨t, hmt, hin, hlt⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : 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

Proof state:
case neg.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this✝ : ∀ 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)⁻¹

Tactic:
exact le_trans (measure_mono <| iInter_subset t n) (hm' n).le

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this✝ : ∀ 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

Tactic:
refine le_antisymm (ge_of_tendsto' this fun n => ?_) ?_

Result:
case neg.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this✝ : ∀ 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 : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this✝ : ∀ 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)

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
have : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r := by
  intro r hs
  have : ∃t, MeasurableSet t ∧ s ⊆ t ∧ m t < r := by simpa [ms, iInf_lt_iff] using hs
  rcases this with ⟨t, hmt, hin, hlt⟩
  exists t

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ⊤
this : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ⊤
r : ℝ≥0∞
hs : r > ms
⊢ ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r

Tactic:
simpa [ms, iInf_lt_iff] using hs

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
simp only [hs]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ⊤
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ⊤