awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
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
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i

Tactic:
obtain hbdd | hbdd := hbdd
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
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
⊢ ∃ (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

Premises used: ENNReal.exists_frequently_lt_of_liminf_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
inl :
  ∀ (q : ℚ) (hq : R < (↑q : ℝ)),
    ∃ (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

Tactic:
obtain ⟨q, hq⟩ := exists_rat_gt R

Premises used: exists_rat_gt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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

Tactic:
⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩

Premises used: Iff.mpr, lt_add_iff_pos_right, zero_lt_one, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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 : ℝ)
inl₁ : ∃ᶠ (i : ι) in l, (↑(q + 1) : ℝ) < x i
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i

Tactic:
refine ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, ?_, ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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 : ℝ)

Tactic:
fun hcon => hR ?_

Premises used: Filter.Frequently, Not
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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 : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑q : ℝ)) x_1), ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ x n < R) x_1
⊢ ∃ᶠ (i : ι) in l, x i < (↑q : ℝ)

Tactic:
refine fun hcon => hR ?_
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x_1 : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x_1 i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l x_1
R : ℝ
hR : ∃ᶠ (n : ι) in l, x_1 n < R
q : ℚ
hq : R < (↑q : ℝ)
hcon : ∀ᶠ (x : ι) in l, ¬(fun (i : ι) ↦ x_1 i < (↑q : ℝ)) x
x : ι
hx : ¬x_1 x < (↑q : ℝ)
⊢ ¬x_1 x < R

Tactic:
not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le

Premises used: Iff.mpr, LT.lt.le, not_lt, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
h₁ h₂ : ∀ (x_1 : ι) (hx : ¬x x_1 < (↑q : ℝ)), ¬x x_1 < R
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ x n < R) x_1

Tactic:
filter_upwards [hcon] with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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 : ℝ)
⊢ ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1

Tactic:
simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd

Premises used: not_exists, Filter.IsBounded, Filter.eventually_map, Filter.IsBoundedUnder
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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

Tactic:
fun hcon => hbdd ↑(q + 1) ?_

Premises used: Rat.cast, Filter.Frequently, HAdd.hAdd, OfNat.ofNat, Not
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
inl : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑(q + 1) : ℝ) < x i) x_1), ∀ᶠ (a : ι) in l, x a ≤ (↑(q + 1) : ℝ)
⊢ ∃ᶠ (i : ι) in l, (↑(q + 1) : ℝ) < x i

Tactic:
refine fun hcon => hbdd ↑(q + 1) ?_

Premises used: Rat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x_1 : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x_1 i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, x_1 n < R
q : ℚ
hq : R < (↑q : ℝ)
hbdd : ∀ (x : ℝ), ¬∀ᶠ (a : ι) in l, x_1 a ≤ x
hcon : ∀ᶠ (x : ι) in l, ¬(fun (i : ι) ↦ (↑(q + 1) : ℝ) < x_1 i) x
x : ι
hx : ¬(↑(q + 1) : ℝ) < x_1 x
⊢ x_1 x ≤ (↑(q + 1) : ℝ)

Tactic:
not_lt.1 hx

Premises used: not_lt, Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
h₁ h₂ : ∀ (x_1 : ι) (hx : ¬(↑(q + 1) : ℝ) < x x_1), x x_1 ≤ (↑(q + 1) : ℝ)
⊢ ∀ᶠ (a : ι) in l, x a ≤ (↑(q + 1) : ℝ)

Tactic:
filter_upwards [hcon] with x hx using not_lt.1 hx
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
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
⊢ ∃ (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

Premises used: ENNReal.exists_frequently_lt_of_liminf_ne_top'
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
inr :
  ∀ (q : ℚ) (hq : (↑q : ℝ) < R),
    ∃ (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

Tactic:
obtain ⟨q, hq⟩ := exists_rat_lt R

Premises used: exists_rat_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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

Tactic:
⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩

Premises used: Iff.mpr, HSub.hSub, zero_lt_one, And.intro, Exists.intro, sub_lt_self_iff, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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) : ℝ)
inr₁ : ∃ᶠ (i : ι) in l, (↑q : ℝ) < x i
⊢ ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < (↑a : ℝ)) ∧ ∃ᶠ (i : ι) in l, (↑b : ℝ) < x i

Tactic:
refine ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
⊢ ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≥ x_1

Tactic:
simp only [IsBoundedUnder, IsBounded, eventually_map, not_exists] at hbdd

Premises used: not_exists, Filter.IsBounded, Filter.eventually_map, Filter.IsBoundedUnder
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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) : ℝ)

Tactic:
fun hcon => hbdd ↑(q - 1) ?_

Premises used: HSub.hSub, Rat.cast, Filter.Frequently, OfNat.ofNat, Not
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
inr : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ x i < (↑(q - 1) : ℝ)) x_1), ∀ᶠ (a : ι) in l, x a ≥ (↑(q - 1) : ℝ)
⊢ ∃ᶠ (i : ι) in l, x i < (↑(q - 1) : ℝ)

Tactic:
refine fun hcon => hbdd ↑(q - 1) ?_

Premises used: HSub.hSub, Rat.cast, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x_1 : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x_1 i)) : ℝ≥0∞)) l) ∞
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x_1 n
q : ℚ
hq : (↑q : ℝ) < R
hbdd : ∀ (x : ℝ), ¬∀ᶠ (a : ι) in l, x_1 a ≥ x
hcon : ∀ᶠ (x : ι) in l, ¬(fun (i : ι) ↦ x_1 i < (↑(q - 1) : ℝ)) x
x : ι
hx : ¬x_1 x < (↑(q - 1) : ℝ)
⊢ x_1 x ≥ (↑(q - 1) : ℝ)

Tactic:
not_lt.1 hx

Premises used: not_lt, Iff.mp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
h₁ h₂ : ∀ (x_1 : ι) (hx : ¬x x_1 < (↑(q - 1) : ℝ)), x x_1 ≥ (↑(q - 1) : ℝ)
⊢ ∀ᶠ (a : ι) in l, x a ≥ (↑(q - 1) : ℝ)

Tactic:
filter_upwards [hcon] with x hx using not_lt.1 hx
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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

Tactic:
fun hcon => hR ?_

Premises used: Filter.Frequently, Not
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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 : ∀ (hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun (i : ι) ↦ (↑q : ℝ) < x i) x_1), ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ R < x n) x_1
⊢ ∃ᶠ (i : ι) in l, (↑q : ℝ) < x i

Tactic:
refine fun hcon => hR ?_
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
l : Filter ι
x_1 : ι → ℝ
hf : Ne (α := ℝ≥0∞) (liminf (fun (i : ι) ↦ (↑((Real.nnabs : (a : ℝ) → ℝ≥0) (x_1 i)) : ℝ≥0∞)) l) ∞
hbdd : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l x_1
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x_1 n
q : ℚ
hq : (↑q : ℝ) < R
hcon : ∀ᶠ (x : ι) in l, ¬(fun (i : ι) ↦ (↑q : ℝ) < x_1 i) x
x : ι
hx : ¬(↑q : ℝ) < x_1 x
⊢ ¬R < x_1 x

Tactic:
not_lt.2 ((not_lt.1 hx).trans hq.le)

Premises used: Iff.mpr, LT.lt.le, not_lt, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
h₁ h₂ : ∀ (x_1 : ι) (hx : ¬(↑q : ℝ) < x x_1), ¬R < x x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun (n : ι) ↦ R < x n) x_1

Tactic:
filter_upwards [hcon] with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
x : ℝ≥0∞
hx : x ≠ ∞
⊢ ∀ (i : ι), f i ≠ ∞

Tactic:
hf
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
x : ℝ≥0∞
hx : x ≠ ∞
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)
⊢ Tendsto (fun (n : ι) ↦ (f n).toReal) fi (𝓝 x.toReal) ↔ Tendsto f fi (𝓝 x)

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ∞
f : (i : ι) → ℝ≥0
⊢ x ≠ ∞

Tactic:
hx
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
fi : Filter ι
x : ℝ≥0∞
hx : x ≠ ∞
f : (i : ι) → ℝ≥0
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∞))
⊢ Tendsto (fun (n : ι) ↦ ENNReal.toReal ((fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) n)) fi (𝓝 x.toReal) ↔
    Tendsto (fun (i : ι) ↦ (↑(f i) : ℝ≥0∞)) fi (𝓝 x)

Tactic:
lift x to ℝ≥0 using hx
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
fi : Filter ι
f : (i : ι) → ℝ≥0
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:
simp [tendsto_coe]

Premises used: ENNReal.tendsto_coe
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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)
rw₁ rw₂ : Tendsto f fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ι) ↦ (f n).toReal) fi (𝓝 0) ↔ Tendsto f fi (𝓝 0)

Tactic:
rw [← ENNReal.toReal_zero, tendsto_toReal_iff hf ENNReal.zero_ne_top]

Premises used: ENNReal.zero_ne_top, ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : EMetricSpace β
a : β
r : ℝ≥0∞
x y : (↑(eball a r) : Type u_2)
rw : edist (↑x : β) a + edist (↑y : β) a < r + r
⊢ edist a (↑x : β) + edist a (↑y : β) < r + r

Tactic:
rw [edist_comm a x, edist_comm a y]

Premises used: PseudoEMetricSpace.edist_comm, Subtype.val
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : EMetricSpace β
a : β
r : ℝ≥0∞
x y : (↑(eball a r) : Type u_2)
⊢ edist (↑x : β) a + edist (↑y : β) a < r + r

Tactic:
ENNReal.add_lt_add x.2 y.2

Premises used: ENNReal.add_lt_add, Subtype.property
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : EMetricSpace β
a : β
r : ℝ≥0∞
x y : (↑(eball a r) : Type u_2)
⊢ edist (↑x : β) a + edist (↑y : β) a < r + r

Tactic:
exact ENNReal.add_lt_add x.2 y.2

Premises used: ENNReal.add_lt_add, Subtype.property
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : EMetricSpace β
a x : β
r : ℝ≥0∞
h : x ∈ eball a r
⊢ 𝓝 x = map (Subtype.val (p := fun (x : β) ↦ x ∈ eball a r)) (𝓝 (Subtype.mk (p := fun (x : β) ↦ x ∈ eball a r) x h))

Tactic:
(map_nhds_subtype_coe_eq_nhds _ <| isOpen_eball.mem_nhds h).symm

Premises used: Metric.isOpen_eball, Set.Mem, setOf, Metric.eball, IsOpen.mem_nhds, map_nhds_subtype_coe_eq_nhds, Eq.symm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
l : Filter β
f : β → α
y : α
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (β := ℝ≥0∞) (fun (x : β) ↦ edist (f x) y) l (𝓝 0)

Tactic:
simp only [Metric.nhds_basis_eball.tendsto_right_iff, Metric.mem_eball,
    @tendsto_order ℝ≥0∞ β _ _, forall_prop_of_false ENNReal.not_lt_zero, forall_const, true_and]

Premises used: tendsto_order, forall_prop_of_false, ENNReal.not_lt_zero, Metric.nhds_basis_eball, forall_const, Filter.HasBasis.tendsto_right_iff, true_and, Metric.mem_eball
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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)
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) < ε
⊢ (∀ ε > 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
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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)

Tactic:
⟨fun N => Metric.ediam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩

Premises used: Set.Ici, Metric.ediam, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
mp₁ : Tendsto (β := ℝ≥0∞) (fun (N : β) ↦ ediam (s '' Ici N)) atTop (𝓝 0)
⊢ ∃ (b : β → ℝ≥0∞), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
refine ⟨fun N => Metric.ediam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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) < ε
n m N : β
hn : N ≤ n
hm : N ≤ m
⊢ edist (s n) (s m) ≤ (fun (N : β) ↦ ediam (s '' Ici N)) N

Tactic:
Metric.edist_le_ediam_of_mem (mem_image_of_mem _ hn) (mem_image_of_mem _ hm)

Premises used: Metric.edist_le_ediam_of_mem, Set.mem_image_of_mem
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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) < ε
n m N : β
hn : N ≤ n
hm : N ≤ m
⊢ edist (s n) (s m) ≤ (fun (N : β) ↦ ediam (s '' Ici N)) N

Tactic:
exact Metric.edist_le_ediam_of_mem (mem_image_of_mem _ hn) (mem_image_of_mem _ hm)

Premises used: Metric.edist_le_ediam_of_mem, Set.mem_image_of_mem
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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)

Tactic:
ENNReal.tendsto_nhds_zero.2 fun ε ε0 => ?_

Premises used: Iff.mpr, ENNReal.tendsto_nhds_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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 : ∀ (ε : ℝ≥0∞) (ε0 : ε > 0), ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε
⊢ Tendsto (β := ℝ≥0∞) (fun (N : β) ↦ ediam (s '' Ici N)) atTop (𝓝 0)

Tactic:
refine ENNReal.tendsto_nhds_zero.2 fun ε ε0 => ?_

Premises used: Iff.mpr, ENNReal.tendsto_nhds_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
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
mp :
  ∀ (N : β) (hN : ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε),
    ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε
⊢ ∀ᶠ (x : β) in atTop, ediam (s '' Ici x) ≤ ε

Tactic:
rcases hs ε ε0 with ⟨N, hN⟩