n : ℕ
hn : n ≥ 1
⊢ (2 + 1 / ↑n)⁻¹ = (fun n => ↑n / (2 * ↑n + 1)) n
⊢ Tendsto (fun n => ↑n / (2 * ↑n + 1)) atTop (𝓝 (2 + 0)⁻¹)
refine' (((tendsto_const_div_atTop_nhds_0_nat 1).const_add (2 : ℝ)).inv₀
  ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr' (eventually_atTop.mpr ⟨1, fun n hn => _⟩)
no goals
n : ℕ
hn : n ≥ 1
⊢ (2 + 1 / ↑n)⁻¹ = (fun n => ↑n / (2 * ↑n + 1)) n
rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]