[GOAL]
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (nhds 0)
[PROOFSTEP]
convert tendsto_algebraMap_inverse_atTop_nhds_0_nat 𝕜
[GOAL]
case h.e'_3.h
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
x✝ : ℕ
⊢ (↑x✝)⁻¹ = (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) x✝
[PROOFSTEP]
simp
