awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + (↑δ : ℝ≥0∞) < (a, b).2
inr : (a, b).1 < x - min ε (↑δ : ℝ≥0∞)
inr₁ : x + min ε (↑δ : ℝ≥0∞) < (a, b).2
⊢ ∃ (i' : ℝ≥0∞), i' ≠ 0 ∧ Icc (x - i') (x + i') ⊆ Ioo (a, b).1 (a, b).2

Tactic:
refine ⟨min ε δ, (lt_min ε0 (coe_pos.2 δ0)).ne', Icc_subset_Ioo ?_ ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + (↑δ : ℝ≥0∞) < (a, b).2
⊢ (a, b).1 < x - min ε (↑δ : ℝ≥0∞)

Tactic:
lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)

Premises used: Iff.mpr, lt_tsub_comm, min_le_left, LE.le.trans_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + (↑δ : ℝ≥0∞) < (a, b).2
⊢ (a, b).1 < x - min ε (↑δ : ℝ≥0∞)

Tactic:
exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)

Premises used: Iff.mpr, lt_tsub_comm, min_le_left, LE.le.trans_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ inr : x + (↑δ : ℝ≥0∞) < (a, b).2
⊢ x + min ε (↑δ : ℝ≥0∞) < (a, b).2

Tactic:
grw [min_le_right]

Premises used: min_le_right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + (↑δ : ℝ≥0∞) < (a, b).2
⊢ x + (↑δ : ℝ≥0∞) < (a, b).2

Tactic:
hδ
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + (↑δ : ℝ≥0∞) < (a, b).2
⊢ x + (↑δ : ℝ≥0∞) < (a, b).2

Tactic:
exact hδ
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ (i : ℝ≥0∞ × ℝ≥0∞), (i.1 < x ∧ x < i.2) ∧ Ioo i.1 i.2 ⊆ Icc (x - ε) (x + ε)

Tactic:
⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
        lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩

Premises used: Set.Ioo_subset_Icc_self, ENNReal.lt_add_right, HSub.hSub, Prod.mk, LT.lt.ne', HAdd.hAdd, ENNReal.sub_lt_self, And.intro, Exists.intro
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ (i : ℝ≥0∞ × ℝ≥0∞), (i.1 < x ∧ x < i.2) ∧ Ioo i.1 i.2 ⊆ Icc (x - ε) (x + ε)

Tactic:
exact ⟨(x - ε, x + ε), ⟨ENNReal.sub_lt_self xt x0.ne' ε0,
        lt_add_right xt ε0⟩, Ioo_subset_Icc_self⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ 0 < x) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)

Tactic:
simpa only [pos_iff_ne_zero] using hasBasis_nhds_of_ne_top' xt

Premises used: ENNReal.hasBasis_nhds_of_ne_top', pos_iff_ne_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x ε : ℝ≥0∞
xt : x ≠ ∞
ε0 : ε ≠ 0
⊢ Icc (x - ε) (x + ε) ∈ 𝓝 x

Tactic:
(hasBasis_nhds_of_ne_top' xt).mem_of_mem ε0

Premises used: ENNReal.hasBasis_nhds_of_ne_top', Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
⊢ 𝓝 x = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 (Icc (x - ε) (x + ε))

Tactic:
(hasBasis_nhds_of_ne_top xt).eq_biInf

Premises used: ENNReal.hasBasis_nhds_of_ne_top, Filter.HasBasis.eq_biInf
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
⊢ 𝓟 (Icc (HSub.hSub (α := ℝ≥0∞) ∞ 1) (HAdd.hAdd (α := ℝ≥0∞) ∞ 1)) ≤ 𝓝 ∞

Tactic:
simpa only [← coe_one, top_sub_coe, top_add, Icc_self, principal_singleton] using pure_le_nhds _

Premises used: ENNReal.top_sub_coe, Set.Icc_self, pure_le_nhds, ENNReal.coe_one, Filter.principal_singleton, top_add
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (𝓝 a)

Tactic:
Tendsto.mono_right ?_ (biInf_le_nhds _)

Premises used: Filter.Tendsto.mono_right, ENNReal.biInf_le_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
refine : Tendsto u f (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 (Icc (a - ε) (a + ε)))
⊢ Tendsto u f (𝓝 a)

Tactic:
refine Tendsto.mono_right ?_ (biInf_le_nhds _)

Premises used: Filter.Tendsto.mono_right, ENNReal.biInf_le_nhds
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto u f (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 (Icc (a - ε) (a + ε)))

Tactic:
simpa only [tendsto_iInf, tendsto_principal]

Premises used: Filter.tendsto_principal, Filter.tendsto_iInf
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Icc (a - ε) (a + ε)

Tactic:
simp only [nhds_of_ne_top ha, tendsto_iInf, tendsto_principal]

Premises used: Filter.tendsto_principal, ENNReal.nhds_of_ne_top, Filter.tendsto_iInf
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
⊢ Tendsto u f (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ≤ ε

Tactic:
nhds_zero_basis_Iic.tendsto_right_iff

Premises used: Set.Mem, setOf, ENNReal.nhds_zero_basis_Iic, Set.Iic, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
rw : (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : α) ↦ a - f n) l (𝓝 0) ↔ Tendsto (fun (n : α) ↦ f n) l (𝓝 a)

Tactic:
rw [ENNReal.tendsto_nhds_zero, ENNReal.tendsto_nhds ha]

Premises used: ENNReal.tendsto_nhds, ENNReal.tendsto_nhds_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

Tactic:
⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
refine_1 :
  ∀ (h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) (ε : ℝ≥0∞) (hε : ε > 0), ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
refine_2 :
  ∀ (h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)) (ε : ℝ≥0∞) (hε : ε > 0), ∀ᶠ (x : α) in l, a - f x ≤ ε
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
h₁ : ∀ (n : α) (hn : a - f n ≤ ε), f n ∈ Icc (a - ε) (a + ε)
⊢ ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

Tactic:
filter_upwards [h ε hε] with n hn
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ f n ∈ Icc (a - ε) (a + ε)

Tactic:
⟨?_, (hfa n).trans (le_add_right le_rfl)⟩

Premises used: le_rfl, Set.Mem, setOf, Set.Icc, And.intro, LE.le.trans, le_add_right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
h₁ : a - ε ≤ f n
⊢ f n ∈ Icc (a - ε) (a + ε)

Tactic:
refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
h₁ : ∀ (hn : a ≤ ε + f n), a ≤ f n + ε
⊢ a - ε ≤ f n

Tactic:
rw [tsub_le_iff_right] at hn ⊢

Premises used: tsub_le_iff_right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a ≤ ε + f n
h₁ h₂ h₃ h₄ : a ≤ ε + f n
⊢ a ≤ f n + ε

Tactic:
rwa [add_comm]

Premises used: add_comm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
h₁ : ∀ (n : α) (hn : f n ∈ Icc (a - ε) (a + ε)), a - f n ≤ ε
⊢ ∀ᶠ (x : α) in l, a - f x ≤ ε

Tactic:
filter_upwards [h ε hε] with n hn
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
⊢ a - ε ≤ f n

Tactic:
have hN_left := hn.1
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a - ε ≤ f n
h₁ : ∀ (hN_left : a ≤ f n + ε), a ≤ ε + f n
⊢ a - f n ≤ ε

Tactic:
rw [tsub_le_iff_right] at hN_left ⊢

Premises used: tsub_le_iff_right
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a ≤ f n + ε
h₁ h₂ h₃ h₄ : a ≤ f n + ε
⊢ a ≤ ε + f n

Tactic:
rwa [add_comm]

Premises used: add_comm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
simp :
  (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)

Tactic:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
simp : (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε

Tactic:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_2
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
rw : (∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero]

Premises used: ENNReal.tendsto_atTop_zero
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε

Tactic:
⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
refine_1 : ∀ (h : ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (n : β), f n ≤ ε
refine_2 : ∀ (h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) (ε : ℝ≥0∞) (hε : ε > 0), ∃ (N : β), ∀ n ≥ N, f n ≤ ε
⊢ (∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε

Tactic:
refine ⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
refine_1 : ∀ (n : β) (hn : ∀ n_1 ≥ n, f n_1 ≤ ε), ∃ (n : β), f n ≤ ε
⊢ ∃ (n : β), f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : ∀ n_1 ≥ n, f n_1 ≤ ε
⊢ ∃ (n : β), f n ≤ ε

Tactic:
⟨n, hn n le_rfl⟩

Premises used: le_rfl, Exists.intro
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : ∀ n_1 ≥ n, f n_1 ≤ ε
⊢ ∃ (n : β), f n ≤ ε

Tactic:
exact ⟨n, hn n le_rfl⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
refine_2 : ∀ (n : β) (hn : f n ≤ ε), ∃ (N : β), ∀ n ≥ N, f n ≤ ε
⊢ ∃ (N : β), ∀ n ≥ N, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : β
hn : f n ≤ ε
⊢ ∃ (N : β), ∀ n ≥ N, f n ≤ ε

Tactic:
⟨n, fun m hm ↦ (hf hm).trans hn⟩

Premises used: Exists.intro, LE.le.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : β
hn : f n ≤ ε
⊢ ∃ (N : β), ∀ n ≥ N, f n ≤ ε

Tactic:
exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
rw : (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε

Tactic:
rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]

Premises used: ENNReal.tendsto_atTop_zero_iff_le_of_antitone
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
mp : (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
mpr : (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε

Tactic:
constructor
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
mp : ∀ (n : β) (hn : f n ≤ min 1 (ε / 2)), ∃ (n : β), f n < ε
⊢ ∃ (n : β), f n < ε

Tactic:
obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
      (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨hε.ne', by finiteness⟩)⟩)

Premises used: Iff.mpr, ENNReal.div_pos_iff, HDiv.hDiv, LT.lt.ne', zero_lt_one, And.intro, OfNat.ofNat, Min.min, lt_min_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
⊢ ∃ (n : β), f n < ε

Tactic:
⟨n, hn.trans_lt ?_⟩

Premises used: Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
mp : min 1 (ε / 2) < ε
⊢ ∃ (n : β), f n < ε

Tactic:
refine ⟨n, hn.trans_lt ?_⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
pos : ∀ (hε_top : ε = ∞), min 1 (ε / 2) < ε
neg : ∀ (hε_top : ¬ε = ∞), min 1 (ε / 2) < ε
⊢ min 1 (ε / 2) < ε

Tactic:
by_cases hε_top : ε = ∞
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ε = ∞
⊢ min 1 (ε / 2) < ε

Tactic:
simp [hε_top]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ min 1 (ε / 2) < ε

Tactic:
(min_le_right _ _).trans_lt ?_

Premises used: min_le_right, LE.le.trans_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
neg : ε / 2 < ε
⊢ min 1 (ε / 2) < ε

Tactic:
refine (min_le_right _ _).trans_lt ?_

Premises used: min_le_right, LE.le.trans_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
neg : ε < ε * 2
⊢ ε / 2 < ε

Tactic:
rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]

Premises used: LT.lt.ne', ENNReal.div_lt_iff, Or.inr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
rw : ε * 1
| ε

Tactic:
rw [← mul_one ε]

Premises used: mul_one
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
neg : ε * 1 < ε * 2
⊢ ε < ε * 2

Tactic:
conv_lhs => rw [← mul_one ε]

Premises used: mul_one
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
neg : LT.lt (α := ℝ≥0∞) 1 2
⊢ ε * 1 < ε * 2

Tactic:
gcongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ LT.lt (α := ℝ≥0∞) 1 2

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
ε : ℝ≥0∞
hε : 0 < ε
mpr : ∀ (n : β) (hn : f n < ε), ∃ (n : β), f n ≤ ε
⊢ ∃ (n : β), f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n < ε
⊢ ∃ (n : β), f n ≤ ε

Tactic:
⟨n, hn.le⟩

Premises used: LT.lt.le, Exists.intro
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
β : Type u_4
inst : Nonempty β
inst_1 : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (n : β), f n < ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n < ε
⊢ ∃ (n : β), f n ≤ ε

Tactic:
exact ⟨n, hn.le⟩
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 (∞, ∞)) (𝓝 (HSub.hSub (α := ℝ≥0∞) ∞ ∞))

Tactic:
simp only [ne_eq, not_true_eq_false, or_self] at h

Premises used: not_true_eq_false, ne_eq, or_self
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
rw : ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, (↑b : ℝ≥0∞)), (↑x : ℝ≥0∞) < a.1 - a.2
⊢ Tendsto (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 (∞, (↑b : ℝ≥0∞))) (𝓝 (∞ - (↑b : ℝ≥0∞)))

Tactic:
rw [top_sub_coe, tendsto_nhds_top_iff_nnreal]

Premises used: ENNReal.top_sub_coe, ENNReal.tendsto_nhds_top_iff_nnreal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, (↑b : ℝ≥0∞)), (↑x : ℝ≥0∞) < a.1 - a.2

Tactic:
fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
      (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_

Premises used: Iff.mpr, lt_add_one, ENNReal.coe_lt_coe, Filter.Eventually.mono, ge_mem_nhds, Filter.Eventually.prod_nhds, lt_mem_nhds, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
refine :
  ∀ (x : ℝ≥0) (y : ℝ≥0∞ × ℝ≥0∞) (hy : (↑(b + 1 + x) : ℝ≥0∞) < y.1 ∧ y.2 ≤ (↑(b + 1) : ℝ≥0∞)), (↑x : ℝ≥0∞) < y.1 - y.2
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (∞, (↑b : ℝ≥0∞)), (↑x : ℝ≥0∞) < a.1 - a.2

Tactic:
refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
      (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_

Premises used: Iff.mpr, lt_add_one, ENNReal.coe_lt_coe, Filter.Eventually.mono, ge_mem_nhds, Filter.Eventually.prod_nhds, lt_mem_nhds, ENNReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : (↑(b + 1 + x) : ℝ≥0∞) < y.1 ∧ y.2 ≤ (↑(b + 1) : ℝ≥0∞)
grw : (↑(b + 1) : ℝ≥0∞) + (↑x : ℝ≥0∞) < y.1
⊢ (↑x : ℝ≥0∞) < y.1 - y.2

Tactic:
grw [lt_tsub_iff_left, hy.2]

Premises used: And.right, lt_tsub_iff_left
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : (↑(b + 1 + x) : ℝ≥0∞) < y.1 ∧ y.2 ≤ (↑(b + 1) : ℝ≥0∞)
⊢ (↑(b + 1) : ℝ≥0∞) + (↑x : ℝ≥0∞) < y.1

Tactic:
hy.1

Premises used: ENNReal.ofNNReal, WithTop.map₂, WithTop.some, And.left, Option.map₂
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
b : ℝ≥0
h : Ne (α := ℝ≥0∞) ∞ ∞ ∨ (↑b : ℝ≥0∞) ≠ ∞
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : (↑(b + 1 + x) : ℝ≥0∞) < y.1 ∧ y.2 ≤ (↑(b + 1) : ℝ≥0∞)
⊢ (↑(b + 1) : ℝ≥0∞) + (↑x : ℝ≥0∞) < y.1

Tactic:
exact hy.1

Premises used: And.left
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a : ℝ≥0
h : (↑a : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ∞ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 - p.2) (𝓝 ((↑a : ℝ≥0∞), ∞)) (𝓝 0)

Tactic:
(tendsto_pure.2 ?_).mono_right (pure_le_nhds _)

Premises used: Iff.mpr, pure_le_nhds, Filter.tendsto_pure, Filter.Tendsto.mono_right