Should field_simp be able to do all the work in this proof?

Stream: general

[Walter Moreira]

I'm trying to prove the equality

$$\frac{\sqrt{2 (2 n) π} \left(\frac{2 n}{e}\right) ^ {2 n}} {\left(\sqrt{2 n π} \left(\frac{n}{e}\right) ^ n\right) ^ 2} = \frac{4 ^ n}{ \sqrt{π n }}$$

This is what I've been able to write:

import Mathlib

open Real
example (n : ℕ) (h : 0 < n) :
     √(2 * (2 * n) * π) * ((2 * n) / rexp 1) ^ (2 * n) /
     (√(2 * n * π) * (n / rexp 1) ^ n) ^ 2
        = 4 ^ n / √(π * (n : ℝ)) := by
  field_simp [mul_pow, <- pow_mul, pow_mul, mul_comm]
  ring_nf
  norm_num [mul_comm (a := n), pow_mul, pi_nonneg]
  ac_rfl

It's not too long, but I feel I might be missing some more instructions for field_simp to do all the work itself.

Why do field_simp and norm_num need those helpers in between? Can someone think of a more elegant way to prove this?

[Ilmārs Cīrulis]

import Mathlib

open Real
example (n : ℕ) (h : 0 < n) :
     √(2 * (2 * n) * π) * ((2 * n) / rexp 1) ^ (2 * n) /
     (√(2 * n * π) * (n / rexp 1) ^ n) ^ 2
        = 4 ^ n / √(π * (n : ℝ)) := by
  ring_nf; field_simp; ring_nf; norm_num; rw [mul_comm n, pow_mul 2]; ring_nf

Edits: restored e in rexp which I accidentally deleted; also last norm_num wasn't necessary.

[Ilmārs Cīrulis]

I mean, this is my try. Not sure if this is more elegant.