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