awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
simp :
  Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp +singlePass only [iInf_comm]

Premises used: iInf_comm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => measure_iUnion_le f)
      (fun _ _ _ _ h => measure_mono h) s

Premises used: MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.measure_mono, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact
    inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => measure_iUnion_le f)
      (fun _ _ _ _ h => measure_mono h) s

Premises used: MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.measure_mono, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : { t : Set α // s ⊆ t ∧ MeasurableSet t }), (m : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)

Tactic:
simp [iInf_subtype, iInf_and, trim_eq_iInf]

Premises used: iInf_subtype, iInf_and, MeasureTheory.OuterMeasure.trim_eq_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
⊢ m.trim.trim = m.trim

Tactic:
trim_eq_trim_iff.2 fun _s => m.trim_eq

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.trim_eq, MeasureTheory.OuterMeasure.trim_eq_trim_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim ⊤) ⊤

Tactic:
top_unique <| le_trim _

Premises used: MeasureTheory.OuterMeasure.le_trim, top_unique
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
h :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) (((trim 0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim 0) 0

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((trim 0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
nonpos_iff_eq_zero.1 <| (measure_mono (subset_univ s)).trans_eq <| trim_eq _ .univ

Premises used: LE.le.trans_eq, Set.subset_univ, MeasureTheory.measure_mono, Iff.mp, MeasureTheory.OuterMeasure.trim_eq, MeasurableSet.univ, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((trim 0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact nonpos_iff_eq_zero.1 <| (measure_mono (subset_univ s)).trans_eq <| trim_eq _ .univ

Premises used: LE.le.trans_eq, Set.subset_univ, MeasureTheory.measure_mono, Iff.mp, MeasureTheory.OuterMeasure.trim_eq, MeasurableSet.univ, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
simp :
  ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i),
    LE.le (α := ℝ≥0∞) (∑' (i : ι), ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i : (a : Set α) → ℝ≥0∞) t)
      (∑' (i_3 : ι), (m i_3 : (a : Set α) → ℝ≥0∞) i)
⊢ LE.le (α := ℝ≥0∞) (((sum fun (i : ι) ↦ (m i).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum m).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [sum_apply, trim_eq_iInf, le_iInf_iff]

Premises used: le_iInf_iff, MeasureTheory.OuterMeasure.sum_apply, MeasureTheory.OuterMeasure.trim_eq_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i),
    LE.le (α := ℝ≥0∞) (∑' (i : ι), ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i : (a : Set α) → ℝ≥0∞) t)
      (∑' (i_3 : ι), (m i_3 : (a : Set α) → ℝ≥0∞) i)

Tactic:
fun t st ht =>
    ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht

Premises used: ENNReal.tsum_le_tsum, iInf_le_of_le, DFunLike.coe, iInf_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i),
    LE.le (α := ℝ≥0∞) (∑' (i : ι), ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i : (a : Set α) → ℝ≥0∞) t)
      (∑' (i_3 : ι), (m i_3 : (a : Set α) → ℝ≥0∞) i)

Tactic:
exact fun t st ht =>
    ENNReal.tsum_le_tsum fun i => iInf_le_of_le t <| iInf_le_of_le st <| iInf_le _ ht

Premises used: ENNReal.tsum_le_tsum, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
simp :
  ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [trim_eq_iInf]

Premises used: MeasureTheory.OuterMeasure.trim_eq_iInf
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
set :
  let ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t;
  ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧
        Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
set ms := ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), m t

Premises used: Set
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
pos : ∀ (hs : ms = ∞), ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
neg : ∀ (hs : ¬ms = ∞), ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms

Tactic:
by_cases hs : ms = ∞
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ms = ∞
pos : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms

Tactic:
simp only [hs]
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ms = ∞
⊢ ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i), Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [iInf_eq_top, ms] at hs

Premises used: iInf_eq_top
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i), Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: Set.subset_univ, Set.univ, And.intro, Exists.intro, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i), Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs_1 : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
⊢ ∃ (t : Set α), MeasurableSet t ∧ s ⊆ t ∧ (m : (a : Set α) → ℝ≥0∞) t < r

Tactic:
simpa [ms, iInf_lt_iff] using hs

Premises used: iInf_lt_iff
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs_1 : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
⊢ ∃ (t : Set α), MeasurableSet t ∧ s ⊆ t ∧ (m : (a : Set α) → ℝ≥0∞) t < r

Tactic:
have : ∃ t, MeasurableSet t ∧ s ⊆ t ∧ m t < r := by simpa [ms, iInf_lt_iff] using hs
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs_1 : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
this : ∃ (t : Set α), MeasurableSet t ∧ s ⊆ t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
rcases :
  ∀ (t : Set α) (hmt : MeasurableSet t) (hin : s ⊆ t) (hlt : (m : (a : Set α) → ℝ≥0∞) t < r),
    ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r

Tactic:
rcases this with ⟨t, hmt, hin, hlt⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs_1 : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
t : Set α
hmt : MeasurableSet t
hin : s ⊆ t
hlt : (m : (a : Set α) → ℝ≥0∞) t < r
exists exists₁ : s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r

Tactic:
exists t
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
⊢ ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r

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
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
n : ℕ
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < ms + (↑n : ℝ≥0∞)⁻¹

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

Premises used: ENNReal.lt_add_right
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
n : ℕ
refine : Ne (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < ms + (↑n : ℝ≥0∞)⁻¹

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

Premises used: ENNReal.lt_add_right
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
n : ℕ
⊢ Ne (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
⊢ ∀ (n : ℕ), ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < ms + (↑n : ℝ≥0∞)⁻¹

Tactic:
have : ∀ n : ℕ, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < ms + (n : ℝ≥0∞)⁻¹ := by
      intro n
      refine this _ (ENNReal.lt_add_right hs ?_)
      simp
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
this : ∀ (n : ℕ), ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < ms + (↑n : ℝ≥0∞)⁻¹
neg :
  ∀ (t : (n : ℕ) → Set α) (hsub : ∀ (n : ℕ), s ⊆ t n) (hm : ∀ (n : ℕ), MeasurableSet (t n))
    (hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹),
    ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms

Tactic:
choose t hsub hm hm' using this
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms

Tactic:
⟨⋂ n, t n, subset_iInter hsub, MeasurableSet.iInter hm, ?_⟩

Premises used: Set.iInter, Set.subset_iInter, And.intro, Exists.intro, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
neg : (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) = ms
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms

Tactic:
refine ⟨⋂ n, t n, subset_iInter hsub, MeasurableSet.iInter hm, ?_⟩
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0))

Tactic:
have : Tendsto (fun n : ℕ => ms + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0)) :=
      tendsto_const_nhds.add ENNReal.tendsto_inv_nat_nhds_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 (ms + 0))
⊢ Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)

Tactic:
rw [add_zero] at this

Premises used: add_zero
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
⊢ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) = ms

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

Premises used: ge_of_tendsto', le_antisymm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
neg : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) ≤ ms + (↑n : ℝ≥0∞)⁻¹
neg₁ : ms ≤ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)
⊢ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) = ms

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

Premises used: ge_of_tendsto', le_antisymm
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
n : ℕ
⊢ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) ≤ ms + (↑n : ℝ≥0∞)⁻¹

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

Premises used: LT.lt.le, MeasureTheory.measure_mono, Set.iInter_subset, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
n : ℕ
⊢ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) ≤ ms + (↑n : ℝ≥0∞)⁻¹

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

Premises used: LT.lt.le, MeasureTheory.measure_mono, Set.iInter_subset, le_trans
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
⊢ ms ≤ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)

Tactic:
iInf_le_of_le (⋂ n, t n) ?_

Premises used: Set.iInter, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
neg :
  LE.le (α := ℝ≥0∞)
    (⨅ (_ : s ⊆ ⋂ (n : ℕ), t n),
        ⨅ (_ : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), t n)), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)
⊢ ms ≤ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)

Tactic:
refine iInf_le_of_le (⋂ n, t n) ?_

Premises used: Set.iInter, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (_ : s ⊆ ⋂ (n : ℕ), t n),
        ⨅ (_ : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), t n)), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)

Tactic:
iInf_le_of_le (subset_iInter hsub) ?_

Premises used: Set.subset_iInter, iInf_le_of_le
-- Module: Mathlib.MeasureTheory.OuterMeasure.Induced
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t
hs : ¬ms = ∞
this_1 : ∀ r > ms, ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
t : (n : ℕ) → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (t n) < ms + (↑n : ℝ≥0∞)⁻¹
this : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
neg :
  LE.le (α := ℝ≥0∞)
    (⨅ (_ : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), t n)), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨅ (_ : s ⊆ ⋂ (n : ℕ), t n),
        ⨅ (_ : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), t n)), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) :
      ℝ≥0∞)
    ((m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞)

Tactic:
refine iInf_le_of_le (subset_iInter hsub) ?_

Premises used: Set.subset_iInter, iInf_le_of_le