case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
obtain ⟨a, hapos, halimit⟩ := stirlingSeq_has_pos_limit_a
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / ↑2 = a ^ 2 / 2
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
have hπ : π / 2 = a ^ 2 / 2 :=
  tendsto_nhds_unique Wallis.tendsto_W_nhds_pi_div_two (second_wallis_limit a hapos.ne' halimit)
no goals
case intro.intro
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / ↑2 = a ^ 2 / 2
⊢ Tendsto (fun n => stirlingSeq n) atTop (𝓝 (Real.sqrt π))
rwa [(div_left_inj' (two_ne_zero' ℝ)).mp hπ, sqrt_sq hapos.le]