case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ ↑n) atTop atTop
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℤ
hn : 0 < n
⊢ Tendsto (fun x => x ^ n) atTop atTop
lift n to ℕ using hn.le
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ n) atTop atTop
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ ↑n) atTop atTop
simp only [zpow_ofNat]
no goals
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ n) atTop atTop
exact tendsto_pow_atTop (Nat.cast_pos.mp hn).ne'