-- Mathlib/Analysis/SpecificLimits/FloorPow.lean
theorem tendsto_div_of_monotone_of_exists_subseq_tendsto_div (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)

Proof state:
case hab
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
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
ε : ℝ
hε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
npos : 0 < n
⊢ u n ≤ ↑n * l + ε * (1 + ε + l) * ↑n

Tactic:
linarith only [hn]

Result:
no goals

Proof state:
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find 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

Result:
no goals

Proof state:
case h₁
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find 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

Result:
no goals

Proof state:
case hab
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find 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

Result:
no goals

Proof state:
case h
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
have Npos : 0 < N := lt_of_lt_of_le Nat.succ_pos' aN

Result:
case h
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n

Proof state:
case H2
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
⊢ c N ∈ image (fun i => c i) (range (a + 1))

Tactic:
apply mem_image_of_mem

Result:
case H2.h
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
h : N < a + 1
⊢ N ∈ range (a + 1)

Proof state:
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 : ℕ := (image (fun i => c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find 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

Result:
no goals