rw [Stirling.stirlingSeq, Stirling.stirlingSeq, centralBinom, two_mul n, cast_add_choose,
  ←two_mul]
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ Stirling.stirlingSeq (2 * n) / Stirling.stirlingSeq n ^ 2 = ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n
case h
this✝¹ : 0 < π
this✝ : (Real.sqrt π)⁻¹ = Real.sqrt π / Real.sqrt π ^ 2
this : Tendsto (fun n => Stirling.stirlingSeq (2 * n)) atTop (𝓝 (Real.sqrt π))
n : ℕ
hn : 0 < n
⊢ ↑(2 * n)! / (Real.sqrt (2 * ↑(2 * n)) * (↑(2 * n) / rexp 1) ^ (2 * n)) /
      (↑n ! / (Real.sqrt (2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2 =
    ↑(2 * n)! / (↑n ! * ↑n !) * Real.sqrt ↑n / 4 ^ n