awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
ht : P t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    ⨅ (_ : u ⊆ t), m t ht
have mpr : ∀ (i : u ⊆ t),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    m t ht
Tactic: refine le_iInf ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄ (_hm : ∀ (i : ℕ), P (f i)), P (⋃ (i : ℕ), f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
h :
  ∀ (t : Set α),
    P t →
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
          ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
        (inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) t
u t : Set α
ht : P t
h2t : u ⊆ t
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    m t ht
have mpr : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((inducedOuterMeasure (P := P) m P0 m0 : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
Tactic: refine le_trans ?_ ((h t ht).trans_eq <| inducedOuterMeasure_eq' _ msU m_mono ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ extend (P := MeasurableSet) m s₁ ≤ extend (P := MeasurableSet) m s₂
have refine : ∀ (i : MeasurableSet s₂), extend (P := MeasurableSet) m s₁ ≤ m s₂ i
Tactic: refine le_iInf ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
⊢ extend (P := MeasurableSet) m s₁ ≤ m s₂ h₂
have this : extend (P := MeasurableSet) m (s₁ ∪ s₂ \ s₁) =
  extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
Tactic: have :=
    extend_union MeasurableSet.empty m0 MeasurableSet.iUnion mU disjoint_sdiff_self_right h₁
      (h₂.diff h₁)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this :
  extend (P := MeasurableSet) m (s₁ ∪ s₂ \ s₁) =
    extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
⊢ extend (P := MeasurableSet) m s₁ ≤ m s₂ h₂
have this₁ : extend (P := MeasurableSet) m s₂ = extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
Tactic: rw [union_diff_cancel hs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
this : extend (P := MeasurableSet) m s₂ = extend (P := MeasurableSet) m s₁ + extend (P := MeasurableSet) m (s₂ \ s₁)
⊢ extend (P := MeasurableSet) m s₁ ≤ m s₂ h₂
have rw : extend (P := MeasurableSet) m s₁ ≤ extend (P := MeasurableSet) m s₂
Tactic: rw [← extend_eq m]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
⊢ ∀ (s : ℕ → Set α), extend (P := MeasurableSet) m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), extend (P := MeasurableSet) m (s i)
have refine : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), m (⋃ (i : ℕ), f i) sorry ≤ ∑' (i : ℕ), m (f i) sorry
Tactic: refine extend_iUnion_le_tsum_nat' MeasurableSet.iUnion ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
have simp : m (⋃ (i : ℕ), disjointed f i) sorry ≤ ∑' (i : ℕ), m (f i) sorry
Tactic: simp +singlePass only [iUnion_disjointed.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ m (⋃ (i : ℕ), disjointed f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
have rw : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), m (disjointed f i) sorry) (∑' (i : ℕ), m (f i) sorry)
Tactic: rw [mU (MeasurableSet.disjointed h) (disjoint_disjointed _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), m (disjointed f i) ⋯) (∑' (i : ℕ), m (f i) ⋯)
have refine : ∀ (i : ℕ), m (disjointed f i) sorry ≤ m (f i) sorry
Tactic: refine ENNReal.tsum_le_tsum fun i => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ m (disjointed f i) ⋯ ≤ m (f i) ⋯
have rw : extend (P := MeasurableSet) m (disjointed f i) ≤ extend (P := MeasurableSet) m (f i)
Tactic: rw [← extend_eq m, ← extend_eq m]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ m.trim ≤ m.trim
have simp : ∀ (s : Set α),
  MeasurableSet s → LE.le (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [le_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [trim_eq _ (h s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m₁ m₂ : OuterMeasure α
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((m₁.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
    LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
  LE.le (α := ℝ≥0∞) ((m₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [trim_eq _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (⨅ (t : Set α), ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), (m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp +singlePass only [iInf_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (trim 0) 0
have h : ∀ (s : Set α),
  Eq (α := ℝ≥0∞) (((trim 0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
ι : Type u_2
m : ι → OuterMeasure α
s : Set α
⊢ LE.le (α := ℝ≥0∞) (((sum fun (i : ι) ↦ (m i).trim : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum m).trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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)
Tactic: simp only [sum_apply, trim_eq_iInf, le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∃ (t : Set α),
    s ⊆ t ∧
      MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: simp only [trim_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
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
have pos : ∀ (hs : ms = ∞), ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
Tactic: by_cases hs : ms = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
have neg : ∀ (hs : ¬ms = ∞), ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
Tactic: by_cases hs : ms = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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 = ∞
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
have pos : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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 = ∞
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have hs₁ : ∀ (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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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 α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
have this : ∃ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
have 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
Tactic: rcases this with ⟨t, hmt, hin, hlt⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
have exists : s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t < r
Tactic: exists t
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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 = ∞
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
have this : ∀ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)⁻¹
have refine : Ne (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0
Tactic: refine this _ (ENNReal.lt_add_right hs ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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 : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)⁻¹
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ (m : (a : Set α) → ℝ≥0∞) t = ms
have 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
Tactic: choose t hsub hm hm' using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
have neg : (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) = ms
Tactic: refine ⟨⋂ n, t n, subset_iInter hsub, MeasurableSet.iInter hm, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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∞)⁻¹
⊢ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) = ms
have this₁ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (hypothesis)
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))
⊢ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) = ms
have this₁ : Tendsto (fun (n : ℕ) ↦ ms + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 ms)
Tactic: rw [add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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
have neg : ∀ (n : ℕ), (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) ≤ ms + (↑n : ℝ≥0∞)⁻¹
Tactic: refine le_antisymm (ge_of_tendsto' this fun n => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)⁻¹
⊢ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) = ms
have neg₁ : ms ≤ (m : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)
Tactic: refine le_antisymm (ge_of_tendsto' this fun n => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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)
have 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∞)
Tactic: refine iInf_le_of_le (⋂ n, t n) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
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∞)
have 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∞)
Tactic: refine iInf_le_of_le (subset_iInter hsub) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.OuterMeasure.Induced (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : Eq (α := ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have rcases : ∀ (t : Set α) (hst : s ⊆ t) (ht : MeasurableSet t)
  (hm : Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m.trim : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
  ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases exists_measurable_superset_eq_trim m s with ⟨t, hst, ht, hm⟩