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
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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
h : N < a + 1
cNM : c N ≤ M
⊢ False

Tactic:
lt_irrefl _ ((cNM.trans hn).trans_lt ncN)

Premises used: lt_irrefl, LE.le.trans, LE.le.trans_lt
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
h : N < a + 1
cNM : c N ≤ M
⊢ False

Tactic:
exact lt_irrefl _ ((cNM.trans hn).trans_lt ncN)

Premises used: lt_irrefl, LE.le.trans, LE.le.trans_lt
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
⊢ a + 1 ≤ N

Tactic:
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)
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
⊢ 0 < N

Tactic:
have Npos : 0 < N := lt_of_lt_of_le Nat.succ_pos' aN
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
⊢ a ≤ N - 1

Tactic:
have aN' : a ≤ N - 1 := (Nat.le_sub_one_iff_lt Npos).mpr aN
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
⊢ N - 1 < N

Tactic:
have : N - 1 < N := Nat.pred_lt Npos.ne'
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
this : N - 1 < N
⊢ c (N - 1) ≤ n

Tactic:
simpa only [not_lt] using Nat.find_min exN this

Premises used: Nat.find_min, not_lt
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
⊢ c (N - 1) ≤ n

Tactic:
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
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
hcd : u (c (N - 1)) ≤ u n
⊢ (↑n : ℝ) * l - u n ≤ (↑(c N) : ℝ) * l - u (c (N - 1))

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
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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ u (c (N - 1)) ≤ u n

Tactic:
hmono cNn
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ u (c (N - 1)) ≤ u n

Tactic:
exact hmono cNn
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
h : (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)
⊢ (↑(c N) : ℝ) * l - u (c (N - 1)) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ) * l - u (c (N - 1))

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
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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ N - 1 + 1 = N

Tactic:
have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
B : N - 1 + 1 = N
⊢ (↑(c N) : ℝ) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ)

Tactic:
simpa [B] using (ha _ aN').1

Premises used: And.left
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ (1 + ε) * (↑(c (N - 1)) : ℝ) * l - u (c (N - 1)) = (↑(c (N - 1)) : ℝ) * l - u (c (N - 1)) + ε * (↑(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
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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ (↑(c (N - 1)) : ℝ) * l - u (c (N - 1)) + ε * (↑(c (N - 1)) : ℝ) * l ≤
    ε * (↑(c (N - 1)) : ℝ) + ε * (↑(c (N - 1)) : ℝ) * l

Tactic:
add_le_add (ha _ aN').2 le_rfl

Premises used: le_rfl, add_le_add, And.right
-- 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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
⊢ ε * (↑(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
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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
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
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)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(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
aN' : a ≤ N - 1
cNn : c (N - 1) ≤ n
l₁ : (↑n : ℝ) * l - u n ≤ (↑(c N) : ℝ) * l - u (c (N - 1))
l₂ : (↑(c N) : ℝ) * l - u (c (N - 1)) ≤ (1 + ε) * (↑(c (N - 1)) : ℝ) * l - u (c (N - 1))
l₃ :
  (1 + ε) * (↑(c (N - 1)) : ℝ) * l - u (c (N - 1)) = (↑(c (N - 1)) : ℝ) * l - u (c (N - 1)) + ε * (↑(c (N - 1)) : ℝ) * l
l₄ : ε * (↑(c (N - 1)) : ℝ) + ε * (↑(c (N - 1)) : ℝ) * l = ε * (1 + l) * (↑(c (N - 1)) : ℝ)
l₅ : ε * (1 + l) * (↑(c (N - 1)) : ℝ) ≤ ε * (1 + l) * (↑n : ℝ)
⊢ (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)

Tactic:
calc
      (n : ℝ) * l - u n ≤ c N * l - u (c (N - 1)) := by
        gcongr
        exact hmono cNn
      _ ≤ (1 + ε) * c (N - 1) * l - u (c (N - 1)) := by
        gcongr
        have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
        simpa [B] using (ha _ aN').1
      _ = c (N - 1) * l - u (c (N - 1)) + ε * c (N - 1) * l := by ring
      _ ≤ ε * c (N - 1) + ε * c (N - 1) * l := add_le_add (ha _ aN').2 le_rfl
      _ = ε * (1 + l) * c (N - 1) := by ring
      _ ≤ ε * (1 + l) * n := by gcongr

Premises used: le_rfl, add_le_add, HSub.hSub, Nat.cast, And.right, HAdd.hAdd, OfNat.ofNat