awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
A : a ≤ N - 1
B : N - 1 + 1 = N
⊢ (↑(c (N - 1 + 1)) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)

Tactic:
have := (ha _ A).1
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
A : a ≤ N - 1
B : N - 1 + 1 = N
this : (↑(c (N - 1 + 1)) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)), (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)

Tactic:
rwa [B] at this
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
⊢ (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)

Tactic:
have IcN : (c N : ℝ) ≤ (1 + ε) * c (N - 1) := by
      have A : a ≤ N - 1 := (Nat.le_sub_one_iff_lt Npos).mpr aN
      have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
      have := (ha _ A).1
      rwa [B] at this
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
hab : u n ≤ u (c N)
⊢ u n - (↑n : ℝ) * l ≤ u (c N) - (↑(c (N - 1)) : ℝ) * l

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 : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ u n ≤ u (c N)

Tactic:
hmono ncN.le

Premises used: LT.lt.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 < ε
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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ u n ≤ u (c N)

Tactic:
exact hmono ncN.le

Premises used: LT.lt.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 < ε
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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ u (c N) - (↑(c (N - 1)) : ℝ) * l = u (c N) - (↑(c N) : ℝ) * l + HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) * l

Tactic:
ring
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
h₁ : u (c N) - (↑(c N) : ℝ) * l ≤ ε * (↑(c N) : ℝ)
h₂ : HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) ≤ ε * (↑(c (N - 1)) : ℝ)
⊢ u (c N) - (↑(c N) : ℝ) * l + HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) * l ≤
    ε * (↑(c N) : ℝ) + ε * (↑(c (N - 1)) : ℝ) * l

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 : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ u (c N) - (↑(c N) : ℝ) * l ≤ ε * (↑(c N) : ℝ)

Tactic:
(ha N (a.le_succ.trans aN)).2

Premises used: Nat.le_succ, And.right, 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 : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ u (c N) - (↑(c N) : ℝ) * l ≤ ε * (↑(c N) : ℝ)

Tactic:
exact (ha N (a.le_succ.trans aN)).2

Premises used: Nat.le_succ, And.right, 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 : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
linarith :
  ε * (↑(c (N - 1)) : ℝ) < HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) →
    ε * (↑(c (N - 1)) : ℝ) - HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) +
        ((↑(c N) : ℝ) - (1 + ε) * (↑(c (N - 1)) : ℝ)) =
      0
⊢ HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) ≤ ε * (↑(c (N - 1)) : ℝ)

Tactic:
linarith only [IcN]
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
bc : 0 ≤ ε
⊢ ε * (↑(c N) : ℝ) + ε * (↑(c (N - 1)) : ℝ) * l ≤ ε * ((1 + ε) * (↑(c (N - 1)) : ℝ)) + ε * (↑(c (N - 1)) : ℝ) * l

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 : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ ε * ((1 + ε) * (↑(c (N - 1)) : ℝ)) + ε * (↑(c (N - 1)) : ℝ) * l = ε * (1 + ε + l) * (↑(c (N - 1)) : ℝ)

Tactic:
ring
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
ha₁ : 0 ≤ ε * (1 + ε + l)
⊢ ε * (1 + ε + l) * (↑(c (N - 1)) : ℝ) ≤ ε * (1 + ε + l) * (↑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 : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - (↑(c n) : ℝ) * l ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ u (c b) - (↑(c b) : ℝ) * l ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
IcN : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
u₁ : u n - (↑n : ℝ) * l ≤ u (c N) - (↑(c (N - 1)) : ℝ) * l
u₂ :
  u (c N) - (↑(c (N - 1)) : ℝ) * l = u (c N) - (↑(c N) : ℝ) * l + HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) * l
u₃ :
  u (c N) - (↑(c N) : ℝ) * l + HSub.hSub (α := ℝ) (↑(c N) : ℝ) (↑(c (N - 1)) : ℝ) * l ≤
    ε * (↑(c N) : ℝ) + ε * (↑(c (N - 1)) : ℝ) * l
u₄ : ε * (↑(c N) : ℝ) + ε * (↑(c (N - 1)) : ℝ) * l ≤ ε * ((1 + ε) * (↑(c (N - 1)) : ℝ)) + ε * (↑(c (N - 1)) : ℝ) * l
u₅ : ε * ((1 + ε) * (↑(c (N - 1)) : ℝ)) + ε * (↑(c (N - 1)) : ℝ) * l = ε * (1 + ε + l) * (↑(c (N - 1)) : ℝ)
u₆ : ε * (1 + ε + l) * (↑(c (N - 1)) : ℝ) ≤ ε * (1 + ε + l) * (↑n : ℝ)
⊢ u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)

Tactic:
calc
      u n - n * l ≤ u (c N) - c (N - 1) * l := by gcongr; exact hmono ncN.le
      _ = u (c N) - c N * l + (c N - c (N - 1)) * l := by ring
      _ ≤ ε * c N + ε * c (N - 1) * l := by
        gcongr
        · exact (ha N (a.le_succ.trans aN)).2
        · linarith only [IcN]
      _ ≤ ε * ((1 + ε) * c (N - 1)) + ε * c (N - 1) * l := by gcongr
      _ = ε * (1 + ε + l) * c (N - 1) := by ring
      _ ≤ ε * (1 + ε + l) * n := by gcongr

Premises used: HMul.hMul, HSub.hSub, Nat.cast, 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
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)

Tactic:
have A : ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop, u n - n * l ≤ ε * (1 + ε + l) * n := by
    intro ε εpos
    rcases hlim (1 + ε) ((lt_add_iff_pos_right _).2 εpos) with ⟨c, cgrowth, ctop, clim⟩
    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
    obtain ⟨a, ha⟩ :
      ∃ a : ℕ, ∀ b : ℕ, a ≤ b → (c (b + 1) : ℝ) ≤ (1 + ε) * c b ∧ u (c b) - c b * l ≤ ε * c b :=
      eventually_atTop.1 (cgrowth.and L)
    let M := ((Finset.range (a + 1)).image fun i => c i).max' (by simp)
    filter_upwards [Ici_mem_atTop M] with n hn
    have exN : ∃ N, n < c N := by
      rcases (tendsto_atTop.1 ctop (n + 1)).exists with ⟨N, hN⟩
      exact ⟨N, by lia⟩
    let N := Nat.find exN
    have ncN : n < c N := Nat.find_spec exN
    have aN : a + 1 ≤ N := by
      by_contra! h
      have cNM : c N ≤ M := by
        apply le_max'
        apply mem_image_of_mem
        exact mem_range.2 h
      exact lt_irrefl _ ((cNM.trans hn).trans_lt ncN)
    have Npos : 0 < N := lt_of_lt_of_le Nat.succ_pos' aN
    have cNn : c (N - 1) ≤ n := by
      have : N - 1 < N := Nat.pred_lt Npos.ne'
      simpa only [not_lt] using Nat.find_min exN this
    have IcN : (c N : ℝ) ≤ (1 + ε) * c (N - 1) := by
      have A : a ≤ N - 1 := (Nat.le_sub_one_iff_lt Npos).mpr aN
      have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
      have := (ha _ A).1
      rwa [B] at this
    calc
      u n - n * l ≤ u (c N) - c (N - 1) * l := by gcongr; exact hmono ncN.le
      _ = u (c N) - c N * l + (c N - c (N - 1)) * l := by ring
      _ ≤ ε * c N + ε * c (N - 1) * l := by
        gcongr
        · exact (ha N (a.le_succ.trans aN)).2
        · linarith only [IcN]
      _ ≤ ε * ((1 + ε) * c (N - 1)) + ε * c (N - 1) * l := by gcongr
      _ = ε * (1 + ε + l) * c (N - 1) := by ring
      _ ≤ ε * (1 + ε + l) * n := by 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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
ε : ℝ
ε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, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
ε : ℝ
ε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
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
ε : ℝ
ε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),
    (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)

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

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat