norm_num1
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)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n =
    ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * (2 ^ 2) ^ 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)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n =
    ↑(2 * n)! * rexp 1 ^ (2 * n) * Real.sqrt 2 ^ 2 * Real.sqrt ↑n ^ 2 * ↑n ^ (2 * n) * ↑n ! ^ 2 * 4 ^ n