n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
n : ℕ
hn : n ≠ 0
⊢ stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
have : 4 = 2 * 2 := by rfl
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (Real.sqrt (2 * ↑n) * (↑n / exp 1) ^ n)) ^ 2) ^ 2 /
        (↑(2 * n)! / (Real.sqrt (2 * ↑(2 * n)) * (↑(2 * n) / exp 1) ^ (2 * n))) ^ 2 *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
rw [stirlingSeq, this, pow_mul, stirlingSeq, Wallis.W_eq_factorial_ratio]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((Real.sqrt (2 * ↑n) ^ 2) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (Real.sqrt (2 * ↑(2 * n)) ^ 2 * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ ((↑n ! / (Real.sqrt (2 * ↑n) * (↑n / exp 1) ^ n)) ^ 2) ^ 2 /
        (↑(2 * n)! / (Real.sqrt (2 * ↑(2 * n)) * (↑(2 * n) / exp 1) ^ (2 * n))) ^ 2 *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
simp_rw [div_pow, mul_pow]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))

n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑(2 * n)

n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((Real.sqrt (2 * ↑n) ^ 2) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (Real.sqrt (2 * ↑(2 * n)) ^ 2 * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
rw [sq_sqrt, sq_sqrt]
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))

n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑(2 * n)

n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n
any_goals positivity
n : ℕ
hn : n ≠ 0
this✝ : 4 = 2 * 2
this : ↑n ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
have : (n : ℝ) ≠ 0 := cast_ne_zero.mpr hn
n : ℕ
hn : n ≠ 0
this✝¹ : 4 = 2 * 2
this✝ : ↑n ≠ 0
this : exp 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this✝ : 4 = 2 * 2
this : ↑n ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
have : exp 1 ≠ 0 := exp_ne_zero 1
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this✝¹ : 4 = 2 * 2
this✝ : ↑n ≠ 0
this : exp 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
have : ((2 * n)! : ℝ) ≠ 0 := cast_ne_zero.mpr (factorial_ne_zero (2 * n))
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
have : 2 * (n : ℝ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero (2 * n)
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2 * (2 * (2 * ↑n) * ((2 * ↑n) ^ (2 * n)) ^ 2) * ↑n *
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 *
      ((2 * ↑n) ^ 2 * ((↑n ^ n) ^ 2) ^ 2 * (↑(2 * n)! ^ 2 * (exp 1 ^ (2 * n)) ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / exp 1 ^ n) ^ 2) ^ 2) /
        (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / exp 1 ^ (2 * n)) ^ 2)) *
      (↑n / (2 * ↑n + 1)) =
    ↑(2 ^ (4 * n)) * ↑(n ! ^ 4) / (↑((2 * n)! ^ 2) * (2 * ↑n + 1))
field_simp
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2 * (2 * (2 * ↑n) * (((2 ^ n) ^ 2) ^ 2 * ((↑n ^ n) ^ 2) ^ 2)) * ↑n *
      (↑(n * 2)! ^ 2 * (2 * ↑n + 1)) =
    (2 ^ n) ^ 4 * ↑n ! ^ 4 *
      (2 ^ 2 * ↑n ^ 2 * ((↑n ^ n) ^ 2) ^ 2 * (↑(n * 2)! ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2) * (2 * ↑n + 1))
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2 * (2 * (2 * ↑n) * ((2 * ↑n) ^ (2 * n)) ^ 2) * ↑n *
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) =
    2 ^ (4 * n) * ↑n ! ^ 4 *
      ((2 * ↑n) ^ 2 * ((↑n ^ n) ^ 2) ^ 2 * (↑(2 * n)! ^ 2 * (exp 1 ^ (2 * n)) ^ 2) * (2 * ↑n + 1))
simp only [mul_pow, mul_comm 2 n, mul_comm 4 n, pow_mul]
no goals
n : ℕ
hn : n ≠ 0
this✝³ : 4 = 2 * 2
this✝² : ↑n ≠ 0
this✝¹ : exp 1 ≠ 0
this✝ : ↑(2 * n)! ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ (↑n ! ^ 2) ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2 * (2 * (2 * ↑n) * (((2 ^ n) ^ 2) ^ 2 * ((↑n ^ n) ^ 2) ^ 2)) * ↑n *
      (↑(n * 2)! ^ 2 * (2 * ↑n + 1)) =
    (2 ^ n) ^ 4 * ↑n ! ^ 4 *
      (2 ^ 2 * ↑n ^ 2 * ((↑n ^ n) ^ 2) ^ 2 * (↑(n * 2)! ^ 2 * ((exp 1 ^ n) ^ 2) ^ 2) * (2 * ↑n + 1))
ring
no goals
n : ℕ
hn : n ≠ 0
⊢ 4 = 2 * 2
rfl
no goals
n : ℕ
hn : n ≠ 0
this : 4 = 2 * 2
⊢ 0 ≤ 2 * ↑n
positivity
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ ¬2 * n + 1 = 0
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ 2 * ↑n + 1 ≠ 0
norm_cast
no goals
n : ℕ
hn : n ≠ 0
this✝² : 4 = 2 * 2
this✝¹ : ↑n ≠ 0
this✝ : exp 1 ≠ 0
this : ↑(2 * n)! ≠ 0
⊢ ¬2 * n + 1 = 0
exact succ_ne_zero (2 * n)