awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * ((↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞)) ≤ (↑(δ' i) : ℝ≥0∞)
have refine : (↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞) / (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i
Tactic: refine mul_le_of_le_div' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞) / (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i
have grw : (↑(δ' i) : ℝ≥0∞) / (↑(w i) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞) / (↑(w i) : ℝ≥0∞)
Tactic: grw [← le_max_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
⊢ ∀ᶠ (b : ℕ) in atTop, (↑b ! : ℝ) / HPow.hPow (α := ℝ) (↑b : ℝ) b ≤ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)
have refine : ∀ (n : ℕ) (hn : 0 < n), (↑n ! : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) n ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ (↑n ! : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) n ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have rcases : ∀ (k : ℕ) (hn : 0 < k.succ),
  (↑k.succ ! : ℝ) / HPow.hPow (α := ℝ) (↑k.succ : ℝ) k.succ ≤ HDiv.hDiv (α := ℝ) 1 (↑k.succ : ℝ)
Tactic: rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
k : ℕ
hn : 0 < k.succ
⊢ (↑k.succ ! : ℝ) / HPow.hPow (α := ℝ) (↑k.succ : ℝ) k.succ ≤ HDiv.hDiv (α := ℝ) 1 (↑k.succ : ℝ)
have rw : (∏ k_1 ∈ Finset.range k, (↑(k_1 + 1 + 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
    ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) ≤
  (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
Tactic: rw [factorial_eq_prod_range_add_one, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
        prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
        Finset.prod_range_succ']
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
k : ℕ
hn : 0 < k.succ
⊢ (∏ k_1 ∈ Finset.range k, (↑(k_1 + 1 + 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
have simp : (∏ x ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤
  (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
Tactic: simp only [one_mul, Nat.cast_add, zero_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
k : ℕ
hn : 0 < k.succ
⊢ (∏ x ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
have refine_1 : ∀ i ∈ Finset.range k, 0 ≤ (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
Tactic: refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
k : ℕ
hn : 0 < k.succ
refine_1 : ∀ i ∈ Finset.range k, 0 ≤ (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
⊢ (∏ x ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
have refine_2 : ∀ i ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤ 1
Tactic: refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ 0 ≤ (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
have hx₁ : x < k
Tactic: rw [Finset.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤ 1
have hx₁ : x < k
Tactic: rw [Finset.mem_range] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤ 1
have refine_2 : HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1 ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
Tactic: refine (div_le_one <| mod_cast hn).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1 ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
have refine_2 : x + 1 + 1 ≤ k + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
α : Type u_4
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorSemiring α
⊢ Tendsto (β := ℕ) (fun (x : α) ↦ ⌈x⌉₊) atTop atTop
have refine : ∀ (x : ℕ), x ≤ ceil.{u_4} (α := α) (↑x : α)
Tactic: refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun (x : R) ↦ (↑⌊a * x⌋₊ : R) / x) atTop (𝓝 a)
have A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 (a - 0))
Tactic: have A : Tendsto (fun x : R ↦ a - x⁻¹) atTop (𝓝 (a - 0)) :=
    tendsto_const_nhds.sub tendsto_inv_atTop_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 (a - 0))
⊢ Tendsto (fun (x : R) ↦ (↑⌊a * x⌋₊ : R) / x) atTop (𝓝 a)
have A₁ : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
Tactic: rw [sub_zero] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun (x : R) ↦ (↑⌊a * x⌋₊ : R) / x) atTop (𝓝 a)
have hgf : ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ (↑⌊a * b⌋₊ : R) / b
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
hgf : ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ (↑⌊a * b⌋₊ : R) / b
⊢ Tendsto (fun (x : R) ↦ (↑⌊a * x⌋₊ : R) / x) atTop (𝓝 a)
have hfh : ∀ᶠ (b : R) in atTop, (↑⌊a * b⌋₊ : R) / b ≤ a
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ (↑⌊a * b⌋₊ : R) / b
have hgf : ∀ (x : R) (hx : x ≥ 1), a - x⁻¹ ≤ (↑⌊a * x⌋₊ : R) / x
Tactic: refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a - x⁻¹ ≤ (↑⌊a * x⌋₊ : R) / x
have hgf : a * x - 1 ≤ (↑⌊a * x⌋₊ : R)
Tactic: simp only [le_div_iff₀ (zero_lt_one.trans_le hx), _root_.sub_mul,
      inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a * x - 1 ≤ (↑⌊a * x⌋₊ : R)
have this : a * x < HAdd.hAdd (α := R) (↑⌊a * x⌋₊ : R) 1
Tactic: have := Nat.lt_floor_add_one (a * x)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
this : a * x < HAdd.hAdd (α := R) (↑⌊a * x⌋₊ : R) 1
⊢ a * x - 1 ≤ (↑⌊a * x⌋₊ : R)
have linarith : (↑⌊a * x⌋₊ : R) < a * x - 1 → a * x - HAdd.hAdd (α := R) (↑⌊a * x⌋₊ : R) 1 + ((↑⌊a * x⌋₊ : R) - (a * x - 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, (↑⌊a * b⌋₊ : R) / b ≤ a
have hfh : ∀ (x : R) (hx : x ≥ 1), (↑⌊a * x⌋₊ : R) / x ≤ a
Tactic: refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ (↑⌊a * x⌋₊ : R) / x ≤ a
have hfh : (↑⌊a * x⌋₊ : R) ≤ a * x
Tactic: rw [div_le_iff₀ (zero_lt_one.trans_le hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun (x : R) ↦ (↑⌈a * x⌉₊ : R) / x) atTop (𝓝 a)
have A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 (a + 0))
Tactic: have A : Tendsto (fun x : R ↦ a + x⁻¹) atTop (𝓝 (a + 0)) :=
    tendsto_const_nhds.add tendsto_inv_atTop_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (hypothesis)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 (a + 0))
⊢ Tendsto (fun (x : R) ↦ (↑⌈a * x⌉₊ : R) / x) atTop (𝓝 a)
have A₁ : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)
Tactic: rw [add_zero] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun (x : R) ↦ (↑⌈a * x⌉₊ : R) / x) atTop (𝓝 a)
have hgf : ∀ᶠ (b : R) in atTop, a ≤ (↑⌈a * b⌉₊ : R) / b
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds A
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)
hgf : ∀ᶠ (b : R) in atTop, a ≤ (↑⌈a * b⌉₊ : R) / b
⊢ Tendsto (fun (x : R) ↦ (↑⌈a * x⌉₊ : R) / x) atTop (𝓝 a)
have hfh : ∀ᶠ (b : R) in atTop, (↑⌈a * b⌉₊ : R) / b ≤ a + b⁻¹
Tactic: apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds A
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a ≤ (↑⌈a * b⌉₊ : R) / b
have hgf : ∀ (x : R) (hx : x ≥ 1), a ≤ (↑⌈a * x⌉₊ : R) / x
Tactic: refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a ≤ (↑⌈a * x⌉₊ : R) / x
have hgf : a * x ≤ (↑⌈a * x⌉₊ : R)
Tactic: rw [le_div_iff₀ (zero_lt_one.trans_le hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, (↑⌈a * b⌉₊ : R) / b ≤ a + b⁻¹
have hfh : ∀ (x : R) (hx : x ≥ 1), (↑⌈a * x⌉₊ : R) / x ≤ a + x⁻¹
Tactic: refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ Tendsto (β := ℕ) (fun (x : ℕ) ↦ x / n) atTop atTop
have rw : LE.le (α := Filter ℕ) (Filter.map (fun (x : ℕ) ↦ x / n) atTop) atTop
Tactic: rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : LE.le (α := Filter ℕ) (Filter.map (fun (x : ℕ) ↦ x / n) atTop) atTop
⊢ Tendsto (β := ℕ) (fun (x : ℕ) ↦ x / n) atTop atTop
have rw₁ : LE.le (α := Filter ℕ) atTop atTop
Tactic: rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
have simp : ((1 + √5) ^ n / HPow.hPow (α := ℝ) 2 n * φ - (1 - √5) ^ n / HPow.hPow (α := ℝ) 2 n * ψ) / √5 /
    (((1 + √5) ^ n / HPow.hPow (α := ℝ) 2 n - (1 - √5) ^ n / HPow.hPow (α := ℝ) 2 n) / √5) =
  (φ - ψ * ((1 - √5) ^ n / HPow.hPow (α := ℝ) 2 n / ((1 + √5) ^ n / HPow.hPow (α := ℝ) 2 n))) /
    (1 - (1 - √5) ^ n / HPow.hPow (α := ℝ) 2 n / ((1 + √5) ^ n / HPow.hPow (α := ℝ) 2 n))
Tactic: simp only [coe_fib_eq, pow_succ, div_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (hypothesis)
Goal:
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ)) atTop (𝓝 φ)
have h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
Tactic: have h₁ n : (fib (n + 1) / fib n : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n) := by
    simp only [coe_fib_eq, pow_succ, div_pow]
    field
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ |ψ / φ| < 1
have rw : -φ < ψ ∧ ψ < φ
Tactic: rw [abs_div, div_lt_one <| by positivity, abs_of_pos goldenRatio_pos, abs_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ -φ < ψ ∧ ψ < φ
have ring_nf : -1 / 2 + √5 * (-1 / 2) < 1 / 2 + √5 * (-1 / 2) ∧ 1 / 2 + √5 * (-1 / 2) < 1 / 2 + √5 * (1 / 2)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (hypothesis)
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ)) atTop (𝓝 φ)
have h₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (ψ / φ) ^ n) atTop (𝓝 0)
Tactic: have h₂ := tendsto_pow_atTop_nhds_zero_of_abs_lt_one (r := ψ / φ) <| by
    rw [abs_div, div_lt_one <| by positivity, abs_of_pos goldenRatio_pos, abs_lt]
    ring_nf
    bound
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ)) atTop (𝓝 φ)
have rw : Tendsto (fun (x : ℕ) ↦ (φ - ψ * (ψ / φ) ^ x) / (1 - (ψ / φ) ^ x)) atTop (𝓝 ((φ - ψ * 0) / HSub.hSub (α := ℝ) 1 0))
Tactic: rw [show φ = (φ - ψ * 0) / (1 - 0) by ring, funext h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(fib n) : ℝ) (↑(fib (n + 1)) : ℝ)) atTop (𝓝 (-ψ))
have h : ∀ (x : ℕ),
  HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(fib (x + 1)) : ℝ) (↑(fib x) : ℝ))⁻¹
Tactic: convert! tendsto_fib_succ_div_fib_atTop.inv₀ (by positivity) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
h :
  ∀ (x : ℕ),
    HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(fib (x + 1)) : ℝ) (↑(fib x) : ℝ))⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(fib n) : ℝ) (↑(fib (n + 1)) : ℝ)) atTop (𝓝 (-ψ))
have h₁ : -ψ = φ⁻¹
Tactic: convert! tendsto_fib_succ_div_fib_atTop.inv₀ (by positivity) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
x : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(fib (x + 1)) : ℝ) (↑(fib x) : ℝ))⁻¹
have h : HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ) = HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ)
Tactic: rw [inv_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Fibonacci (goal)
Goal:
⊢ -ψ = φ⁻¹
have h : -ψ = -ψ
Tactic: rw [inv_goldenRatio]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
⊢ 0 ≤ l
have rcases : ∀ (c : ℕ → ℕ),
  (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑(c n) : ℝ)) →
    ∀ (ctop : Tendsto c atTop atTop) (clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)), 0 ≤ l
Tactic: rcases hlim 2 one_lt_two with ⟨c, _, ctop, clim⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
c : ℕ → ℕ
left : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
⊢ 0 ≤ l
have this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ u 0 / (↑(c n) : ℝ)) atTop (𝓝 0)
Tactic: have : Tendsto (fun n => u 0 / c n) atTop (𝓝 0) :=
      tendsto_const_nhds.div_atTop (tendsto_natCast_atTop_iff.2 ctop)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
c : ℕ → ℕ
left : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ u 0 / (↑(c n) : ℝ)) atTop (𝓝 0)
⊢ 0 ≤ l
have apply : ∀ (n : ℕ), u 0 / (↑(c n) : ℝ) ≤ u (c n) / (↑(c n) : ℝ)
Tactic: apply le_of_tendsto_of_tendsto' this clim fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
c : ℕ → ℕ
left : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ u 0 / (↑(c n) : ℝ)) atTop (𝓝 0)
n : ℕ
⊢ u 0 / (↑(c n) : ℝ) ≤ u (c n) / (↑(c n) : ℝ)
have hab : u 0 ≤ u (c n)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 l)
have lnonneg : 0 ≤ l
Tactic: have lnonneg : 0 ≤ l := by
    rcases hlim 2 one_lt_two with ⟨c, _, ctop, clim⟩
    have : Tendsto (fun n => u 0 / c n) atTop (𝓝 0) :=
      tendsto_const_nhds.div_atTop (tendsto_natCast_atTop_iff.2 ctop)
    apply le_of_tendsto_of_tendsto' this clim fun n => ?_
    gcongr
    exact hmono zero_le
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
have rcases : ∀ (c : ℕ → ℕ) (cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ))
  (ctop : Tendsto c atTop atTop) (clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)),
  ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
Tactic: rcases hlim (1 + ε) ((lt_add_iff_pos_right _).2 εpos) with ⟨c, cgrowth, ctop, clim⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
have clim₁ : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
Tactic: rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ,
        Asymptotics.isLittleO_iff] at clim
Cleared hypotheses: clim