awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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

Tactic:
eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 : ∀ (x : R) (hx : x ≥ 1), a ≤ (↑⌈a * x⌉₊ : R) / x
⊢ ∀ᶠ (b : R) in atTop, a ≤ (↑⌈a * b⌉₊ : R) / b

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
hgf : a * x ≤ (↑⌈a * x⌉₊ : R)
⊢ a ≤ (↑⌈a * x⌉₊ : R) / x

Tactic:
rw [le_div_iff₀ (zero_lt_one.trans_le hx)]

Premises used: zero_lt_one, LT.lt.trans_le, le_div_iff₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)

Tactic:
Nat.le_ceil _

Premises used: Nat.le_ceil
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)

Tactic:
exact Nat.le_ceil _

Premises used: Nat.le_ceil
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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⁻¹

Tactic:
eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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)
hfh : ∀ (x : R) (hx : x ≥ 1), (↑⌈a * x⌉₊ : R) / x ≤ a + x⁻¹
⊢ ∀ᶠ (b : R) in atTop, (↑⌈a * b⌉₊ : R) / b ≤ a + b⁻¹

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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 + x⁻¹

Tactic:
simp [div_le_iff₀ (zero_lt_one.trans_le hx), inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne',
      (Nat.ceil_lt_add_one (mul_nonneg ha (zero_le_one.trans hx))).le, add_mul]

Premises used: add_mul, mul_nonneg, div_le_iff₀, Nat.ceil_lt_add_one, LT.lt.le, zero_le_one, LT.lt.ne', zero_lt_one, LT.lt.trans_le, LE.le.trans, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
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
⊢ Tendsto (β := R) (fun (x : R) ↦ (↑⌈x⌉₊ : R) / x) atTop (𝓝 1)

Tactic:
simpa using tendsto_nat_ceil_mul_div_atTop (zero_le_one' R)

Premises used: zero_le_one', tendsto_nat_ceil_mul_div_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
hn : n ≠ 0
rw : LE.le (α := Filter ℕ) (Filter.map (fun (x : ℕ) ↦ x / n) atTop) atTop
rw₁ rw₂ : LE.le (α := Filter ℕ) atTop atTop
⊢ Tendsto (β := ℕ) (fun (x : ℕ) ↦ x / n) atTop atTop

Tactic:
rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]

Premises used: Filter.Tendsto, Filter.map_div_atTop_eq_nat, Ne.bot_lt
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
n : ℕ
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))
⊢ HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)

Tactic:
simp only [coe_fib_eq, pow_succ, div_pow]

Premises used: pow_succ, Real.coe_fib_eq, div_pow
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
n : ℕ
⊢ ((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:
field
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
⊢ ∀ (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
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ 0 < |φ|

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
rw : -φ < ψ ∧ ψ < φ
⊢ |ψ / φ| < 1

Tactic:
rw [abs_div, div_lt_one <| by positivity, abs_of_pos goldenRatio_pos, abs_lt]

Premises used: abs_div, Real.goldenRatio_pos, div_lt_one, abs_lt, abs_of_pos
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
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
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ -1 / 2 + √5 * (-1 / 2) < 1 / 2 + √5 * (-1 / 2) ∧ 1 / 2 + √5 * (-1 / 2) < 1 / 2 + √5 * (1 / 2)

Tactic:
bound
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ 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
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ φ = (φ - ψ * 0) / HSub.hSub (α := ℝ) 1 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (ψ / φ) ^ n) atTop (𝓝 0)
rw : Tendsto (fun (x : ℕ) ↦ (φ - ψ * (ψ / φ) ^ x) / (1 - (ψ / φ) ^ x)) atTop (𝓝 ((φ - ψ * 0) / HSub.hSub (α := ℝ) 1 0))
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ)) atTop (𝓝 φ)

Tactic:
rw [show φ = (φ - ψ * 0) / (1 - 0) by ring, funext h₁]

Premises used: funext
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ HSub.hSub (α := ℝ) 1 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h₁ : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) (↑(fib (n + 1)) : ℝ) (↑(fib n) : ℝ) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun (x : ℕ) ↦ (φ - ψ * (ψ / φ) ^ x) / (1 - (ψ / φ) ^ x)) atTop (𝓝 ((φ - ψ * 0) / HSub.hSub (α := ℝ) 1 0))

Tactic:
exact const_sub _ (const_mul _ h₂) |>.div (const_sub _ h₂) <| by simp

Premises used: Filter.Tendsto.div, Filter.Tendsto.const_sub, Filter.Tendsto.const_mul
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
⊢ φ ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h :
  ∀ (x : ℕ),
    HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(fib (x + 1)) : ℝ) (↑(fib x) : ℝ))⁻¹
h₁ : -ψ = φ⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(fib n) : ℝ) (↑(fib (n + 1)) : ℝ)) atTop (𝓝 (-ψ))

Tactic:
convert! tendsto_fib_succ_div_fib_atTop.inv₀ (by positivity) using 2

Premises used: Filter.Tendsto.inv₀, tendsto_fib_succ_div_fib_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
x : ℕ
h h₁ : HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ) = HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(fib x) : ℝ) (↑(fib (x + 1)) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(fib (x + 1)) : ℝ) (↑(fib x) : ℝ))⁻¹

Tactic:
rw [inv_div]

Premises used: inv_div
-- Module: Mathlib.Analysis.SpecificLimits.Fibonacci
Goal:
h h₁ : -ψ = -ψ
⊢ -ψ = φ⁻¹

Tactic:
rw [inv_goldenRatio]

Premises used: Real.inv_goldenRatio
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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)
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
⊢ 0 ≤ l

Tactic:
rcases hlim 2 one_lt_two with ⟨c, _, ctop, clim⟩

Premises used: one_lt_two, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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)
⊢ 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)
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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)
apply : ∀ (n : ℕ), u 0 / (↑(c n) : ℝ) ≤ u (c n) / (↑(c n) : ℝ)
⊢ 0 ≤ l

Tactic:
apply le_of_tendsto_of_tendsto' this clim fun n => ?_

Premises used: le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ℕ
hab : u 0 ≤ u (c n)
⊢ u 0 / (↑(c n) : ℝ) ≤ u (c n) / (↑(c n) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 ≤ u (c n)

Tactic:
hmono zero_le

Premises used: zero_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 ≤ u (c n)

Tactic:
exact hmono zero_le

Premises used: zero_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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

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
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 < ε
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 : ℝ)
⊢ ∀ᶠ (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⟩

Premises used: Iff.mpr, lt_add_iff_pos_right, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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)
⊢ ∀ ⦃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

Premises used: Real, Asymptotics.isLittleO_one_iff, Asymptotics.isLittleO_iff, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
h :
  ∀ (n : ℕ) (hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1) (cnpos' : n ∈ c ⁻¹' Set.Ioi 0),
    u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)

Tactic:
filter_upwards [clim εpos, ctop (Ioi_mem_atTop 0)] with n hn cnpos'

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
⊢ 0 < c n

Tactic:
have cnpos : 0 < c n := cnpos'
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ u (c n) - (↑(c n) : ℝ) * l = (u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ)

Tactic:
field
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
hbc : u (c n) / (↑(c n) : ℝ) - l ≤ ε
⊢ (u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ) ≤ ε * (↑(c n) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ u (c n) / (↑(c n) : ℝ) - l ≤ ε

Tactic:
(le_abs_self _).trans ?_

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
hbc : |u (c n) / (↑(c n) : ℝ) - l| ≤ ε
⊢ u (c n) / (↑(c n) : ℝ) - l ≤ ε

Tactic:
refine (le_abs_self _).trans ?_

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ |u (c n) / (↑(c n) : ℝ) - l| ≤ ε

Tactic:
simpa using hn
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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 : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
u₁ : u (c n) - (↑(c n) : ℝ) * l = (u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ)
u₂ : (u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ) ≤ ε * (↑(c n) : ℝ)
⊢ u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)

Tactic:
calc
        u (c n) - c n * l = (u (c n) / c n - l) * c n := by field
        _ ≤ ε * c n := by
          gcongr
          refine (le_abs_self _).trans ?_
          simpa using hn

Premises used: HSub.hSub, HDiv.hDiv, Nat.cast
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
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) : ℝ)

Tactic:
have L : ∀ᶠ n in atTop, u (c n) - c n * l ≤ ε * c n := by
      rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ,
        Asymptotics.isLittleO_iff] at clim
      filter_upwards [clim εpos, ctop (Ioi_mem_atTop 0)] with n hn cnpos'
      have cnpos : 0 < c n := cnpos'
      calc
        u (c n) - c n * l = (u (c n) / c n - l) * c n := by field
        _ ≤ ε * c n := by
          gcongr
          refine (le_abs_self _).trans ?_
          simpa using hn