awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (i : ι) ↦ |x i|
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have hbdd₁ : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x ∨ ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
Tactic: rw [isBoundedUnder_le_abs, not_and_or] at hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x ∨ ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inl : ∀ (hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x),
  ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
Tactic: obtain hbdd | hbdd := hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x ∨ ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
inl :
  ∀ (hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x),
    ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inr : ∀ (hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x),
  ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
Tactic: obtain hbdd | hbdd := hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inl : ∀ (R : ℝ) (hR : ∃ᶠ (n : ι) in l, x n < R),
  ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
Tactic: obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top hf
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inl : ∀ (q : ℚ) (hq : R < (↑q : ℝ)),
  ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
Tactic: obtain ⟨q, hq⟩ := exists_rat_gt R
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inl : ∃ᶠ (i : ι) in l, x i < (↑q : ℝ)
Tactic: refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
inl : ∃ᶠ (i : ι) in l, x i < (↑q : ℝ)
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inl₁ : ∃ᶠ (i : ι) in l, (↑(q + 1) : ℝ) < x i
Tactic: refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
⊢ ∃ᶠ (i : ι) in l, x i < (↑q : ℝ)
have inl : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑q : ℝ)) x_1), ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ x n < R) x_1
Tactic: refine fun hcon => hR ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑q : ℝ)) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ x n < R) x_1
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ x i < (↑q : ℝ)) x_3) x_2} x_1 →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (n : ι) ↦ x n < R) x_3) x_2} x_1}
    a
Tactic: filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑q : ℝ)) x_1
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ x i < (↑q : ℝ)) x_3) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (n : ι) ↦ x n < R) x_3) x_2} x_1}
      a
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ x n < R) x_1
have h₁ : ∀ (a : ι), ¬x a < (↑q : ℝ) → ¬x a < R
Tactic: filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
⊢ ∃ᶠ (i : ι) in l, (↑(q + 1) : ℝ) < x i
have hbdd₁ : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
Tactic: simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
⊢ ∃ᶠ (i : ι) in l, (↑(q + 1) : ℝ) < x i
have inl : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑(q + 1) : ℝ) < x i) x_1), ∀ᶠ (a : ι) in l, x a ≤ (↑(q + 1) : ℝ)
Tactic: refine fun hcon => hbdd ↑(q + 1) ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑(q + 1) : ℝ) < x i) x_1
⊢ ∀ᶠ (a : ι) in l, x a ≤ (↑(q + 1) : ℝ)
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ (↑(q + 1) : ℝ) < x i) x_3) x_2} x_1 →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ x a ≤ (↑(q + 1) : ℝ)) x_2} x_1}
    a
Tactic: filter_upwards [hcon] with x hx using not_lt.1 hx
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < (↑q : ℝ)
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑(q + 1) : ℝ) < x i) x_1
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ (↑(q + 1) : ℝ) < x i) x_3) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ x a ≤ (↑(q + 1) : ℝ)) x_2} x_1}
      a
⊢ ∀ᶠ (a : ι) in l, x a ≤ (↑(q + 1) : ℝ)
have h₁ : ∀ (a : ι), ¬(↑(q + 1) : ℝ) < x a → x a ≤ (↑(q + 1) : ℝ)
Tactic: filter_upwards [hcon] with x hx using not_lt.1 hx
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inr : ∀ (R : ℝ) (hR : ∃ᶠ (n : ι) in l, R < x n),
  ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
Tactic: obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top' hf
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inr : ∀ (q : ℚ) (hq : (↑q : ℝ) < R),
  ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
Tactic: obtain ⟨q, hq⟩ := exists_rat_lt R
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inr : ∃ᶠ (i : ι) in l, x i < (↑(q - 1) : ℝ)
Tactic: refine ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
inr : ∃ᶠ (i : ι) in l, x i < (↑(q - 1) : ℝ)
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i
have inr₁ : ∃ᶠ (i : ι) in l, (↑q : ℝ) < x i
Tactic: refine ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
⊢ ∃ᶠ (i : ι) in l, x i < (↑(q - 1) : ℝ)
have hbdd₁ : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≥ x_1
Tactic: simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≥ x_1
⊢ ∃ᶠ (i : ι) in l, x i < (↑(q - 1) : ℝ)
have inr : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑(q - 1) : ℝ)) x_1), ∀ᶠ (a : ι) in l, x a ≥ (↑(q - 1) : ℝ)
Tactic: refine fun hcon => hbdd ↑(q - 1) ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≥ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑(q - 1) : ℝ)) x_1
⊢ ∀ᶠ (a : ι) in l, x a ≥ (↑(q - 1) : ℝ)
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ x i < (↑(q - 1) : ℝ)) x_3) x_2} x_1 →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ x a ≥ (↑(q - 1) : ℝ)) x_2} x_1}
    a
Tactic: filter_upwards [hcon] with x hx using not_lt.1 hx
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≥ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑(q - 1) : ℝ)) x_1
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ x i < (↑(q - 1) : ℝ)) x_3) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (a : ι) ↦ x a ≥ (↑(q - 1) : ℝ)) x_2} x_1}
      a
⊢ ∀ᶠ (a : ι) in l, x a ≥ (↑(q - 1) : ℝ)
have h₁ : ∀ (a : ι), ¬x a < (↑(q - 1) : ℝ) → x a ≥ (↑(q - 1) : ℝ)
Tactic: filter_upwards [hcon] with x hx using not_lt.1 hx
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
⊢ ∃ᶠ (i : ι) in l, (↑q : ℝ) < x i
have inr : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑q : ℝ) < x i) x_1), ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ R < x n) x_1
Tactic: refine fun hcon => hR ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑q : ℝ) < x i) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ R < x n) x_1
have h : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x_1 : ι |
      Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ (↑q : ℝ) < x i) x_3) x_2} x_1 →
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (n : ι) ↦ R < x n) x_3) x_2} x_1}
    a
Tactic: filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : (↑q : ℝ) < R
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑q : ℝ) < x i) x_1
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (i : ι) ↦ (↑q : ℝ) < x i) x_3) x_2} x_1 →
          Membership.mem (γ := Set ι) {x_2 : ι | (fun (x_3 : ι) ↦ ¬(fun (n : ι) ↦ R < x n) x_3) x_2} x_1}
      a
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ R < x n) x_1
have h₁ : ∀ (a : ι), ¬(↑q : ℝ) < x a → ¬R < x a
Tactic: filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
x : ℝ≥0∞
hx : x ≠ ∞
⊢ Tendsto (fun (n : ι) ↦ (f n).toReal) fi (𝓝 x.toReal) ↔ Tendsto f fi (𝓝 x)
have lift : ∀ (f : (i : ι) → ℝ≥0),
  Tendsto (fun (n : ι) ↦ ENNReal.toReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) n)) fi (𝓝 x.toReal) ↔
    Tendsto (fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) fi (𝓝 x)
Tactic: lift f to ι → ℝ≥0 using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ∞
f : (i : ι) → ℝ≥0
⊢ Tendsto (fun (n : ι) ↦ ENNReal.toReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) n)) fi (𝓝 x.toReal) ↔
    Tendsto (fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) fi (𝓝 x)
have lift : ∀ (x : ℝ≥0),
  Tendsto (fun (n : ι) ↦ ENNReal.toReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) n)) fi (𝓝 (↑x : ℝ≥0∞).toReal) ↔
    Tendsto (fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) fi (𝓝 (↑x : ℝ≥0∞))
Tactic: lift x to ℝ≥0 using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ (f n).toReal) fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)
have rw : Tendsto (fun (n : ι) ↦ (f n).toReal) fi (𝓝 (ENNReal.toReal 0)) ↔ Tendsto f fi (𝓝 0)
Tactic: rw [← ENNReal.toReal_zero, tendsto_toReal_iff hf ENNReal.zero_ne_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
rw : Tendsto (fun (n : ι) ↦ (f n).toReal) fi (𝓝 (ENNReal.toReal 0)) ↔ Tendsto f fi (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ (f n).toReal) fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)
have rw₁ : Tendsto f fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)
Tactic: rw [← ENNReal.toReal_zero, tendsto_toReal_iff hf ENNReal.zero_ne_top]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
β : Type u_2
inst : EMetricSpace β
a : β
r : ℝ≥0∞
x y : (↑(eball a r) : Type u_2)
⊢ edist a (↑x : β) + edist a (↑y : β) < r + r
have rw : edist (↑x : β) a + edist (↑y : β) a < r + r
Tactic: rw [edist_comm a x, edist_comm a y]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
⊢ (∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε) ↔
    ∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
have mp : (∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε) →
  ∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
mp :
  (∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε) →
    ∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
⊢ (∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε) ↔
    ∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
have mpr : (∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)) →
  ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
have mp : ∀ (n m N : β) (hn : N ≤ n) (hm : N ≤ m), edist (s n) (s m) ≤ (fun (N : β) ↦ ediam (s '' Ici N)) N
Tactic: refine ⟨fun N => Metric.ediam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
mp : ∀ (n m N : β) (hn : N ≤ n) (hm : N ≤ m), edist (s n) (s m) ≤ (fun (N : β) ↦ ediam (s '' Ici N)) N
⊢ ∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
have mp₁ : Tendsto (β := ℝ≥0∞) (fun (N : β) ↦ ediam (s '' Ici N)) atTop (𝓝 0)
Tactic: refine ⟨fun N => Metric.ediam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (N : β) ↦ ediam (s '' Ici N)) atTop (𝓝 0)
have mp : ∀ (ε : ℝ≥0∞) (ε0 : ε > 0), ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε
Tactic: refine ENNReal.tendsto_nhds_zero.2 fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε
have mp : ∀ (N : β) (hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε),
  ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε
Tactic: rcases hs ε ε0 with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
hs : ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
ε : ℝ≥0∞
ε0 : ε > 0
N : β
hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
⊢ ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε
have mp : ∀ (n : β) (hn : N ≤ n), ∀ x ∈ s '' Ici n, ∀ y ∈ s '' Ici n, edist x y ≤ ε
Tactic: refine (eventually_ge_atTop N).mono fun n hn => Metric.ediam_le ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
have this : ∀ᶠ (n : β) in atTop, b n < ε
Tactic: have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
have mpr : ∀ (N : β) (hN : b N < ε), ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
Tactic: rcases this.exists with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε
have mpr : ∀ (m : β) (hm : N ≤ m) (n : β) (hn : N ≤ n), edist (s m) (s n) < ε
Tactic: refine ⟨N, fun m hm n hn => ?_⟩