u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
⊢ ∀ (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)
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
⊢ Tendsto (fun n => u n / ↑n) atTop (𝓝 l)
apply tendsto_div_of_monotone_of_exists_subseq_tendsto_div u l hmono
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 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)
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
⊢ ∀ (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)
intro a ha
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < 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)
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 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)
obtain ⟨k, hk⟩ : ∃ k, c k < a := ((tendsto_order.1 clim).2 a ha).exists
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < 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)
refine'
  ⟨fun n => ⌊c k ^ n⌋₊, _,
    (tendsto_nat_floor_atTop (α := ℝ)).comp (tendsto_pow_atTop_atTop_of_one_lt (cone k)), hc k⟩
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
have H : ∀ n : ℕ, (0 : ℝ) < ⌊c k ^ n⌋₊ := by
  intro n
  refine' zero_lt_one.trans_le _
  simp only [Real.rpow_nat_cast, Nat.one_le_cast, Nat.one_le_floor_iff,
    one_le_pow_of_one_le (cone k).le n]
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
B : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
have B : Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / ⌊c k ^ n⌋₊) atTop (𝓝 (c k)) := by
  simp only [one_mul, div_one] at A
  convert A using 1
  ext1 n
  field_simp [(zero_lt_one.trans (cone k)).ne', (H n).ne']
  ring
case h
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
B : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
n : ℕ
hn : ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊ < a
⊢ ↑⌊c k ^ (n + 1)⌋₊ ≤ a * ↑⌊c k ^ n⌋₊
case intro
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
B : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
⊢ ∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
filter_upwards [(tendsto_order.1 B).2 a hk]with n hn
no goals
case h
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
B : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
n : ℕ
hn : ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊ < a
⊢ ↑⌊c k ^ (n + 1)⌋₊ ≤ a * ↑⌊c k ^ n⌋₊
exact (div_le_iff (H n)).1 hn.le
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ 0 < ↑⌊c k ^ n⌋₊
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
⊢ ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
intro n
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ 1 ≤ ↑⌊c k ^ n⌋₊
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ 0 < ↑⌊c k ^ n⌋₊
refine' zero_lt_one.trans_le _
no goals
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ 1 ≤ ↑⌊c k ^ n⌋₊
simp only [Real.rpow_nat_cast, Nat.one_le_cast, Nat.one_le_floor_iff,
  one_le_pow_of_one_le (cone k).le n]
case refine'_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1)) atTop (𝓝 1)

case refine'_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => ↑⌊c k ^ n⌋₊ / c k ^ n) atTop (𝓝 1)
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
refine' Tendsto.div (Tendsto.mul _ tendsto_const_nhds) _ one_ne_zero
case refine'_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => c k ^ (n + 1)) atTop atTop
case refine'_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1)) atTop (𝓝 1)
refine' tendsto_nat_floor_div_atTop.comp _
no goals
case refine'_1
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => c k ^ (n + 1)) atTop atTop
exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)
case refine'_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => c k ^ n) atTop atTop
case refine'_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => ↑⌊c k ^ n⌋₊ / c k ^ n) atTop (𝓝 1)
refine' tendsto_nat_floor_div_atTop.comp _
no goals
case refine'_2
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
⊢ Tendsto (fun n => c k ^ n) atTop atTop
exact tendsto_pow_atTop_atTop_of_one_lt (cone k)
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
⊢ Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))
⊢ Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
simp only [one_mul, div_one] at A
case h.e'_3
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
⊢ (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) = fun n =>
    ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
⊢ Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))
convert A using 1
case h.e'_3.h
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
n : ℕ
⊢ ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊ = ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)
case h.e'_3
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
⊢ (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) = fun n =>
    ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)
ext1 n
case h.e'_3.h
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
n : ℕ
⊢ ↑⌊c k ^ (n + 1)⌋₊ * (c k ^ (n + 1) * ↑⌊c k ^ n⌋₊) = ↑⌊c k ^ (n + 1)⌋₊ * c k * c k ^ n * ↑⌊c k ^ n⌋₊
case h.e'_3.h
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
n : ℕ
⊢ ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊ = ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)
field_simp [(zero_lt_one.trans (cone k)).ne', (H n).ne']
no goals
case h.e'_3.h
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊
A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (c k))
n : ℕ
⊢ ↑⌊c k ^ (n + 1)⌋₊ * (c k ^ (n + 1) * ↑⌊c k ^ n⌋₊) = ↑⌊c k ^ (n + 1)⌋₊ * c k * c k ^ n * ↑⌊c k ^ n⌋₊
ring