-- Mathlib/Data/Real/Pi/Wallis.lean
theorem W_eq_factorial_ratio (n : ℕ) :
    W n = 2 ^ (4 * n) * n ! ^ 4 / ((2 * n)! ^ 2 * (2 * n + 1))

Proof state:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ∏ i ∈ range (n + 1), (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Tactic:
rw [prod_range_succ, IH, _root_.div_mul_div_comm, _root_.div_mul_div_comm]

Result:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) /
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Proof state:
case succ.refine_2
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1) ≠ 0

Tactic:
exact ne_of_gt (by positivity)

Result:
no goals

Proof state:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 * (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Tactic:
simp_rw [Nat.mul_succ, Nat.factorial_succ, pow_succ]

Result:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! ^ 0 * ↑n ! * ↑n ! * ↑n ! * ↑n !) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) ^ 0 * ↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) *
          ↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) *
        (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * n) * 2 * 2 * 2 * 2 *
        (↑((n + 1) * n !) ^ 0 * ↑((n + 1) * n !) * ↑((n + 1) * n !) * ↑((n + 1) * n !) * ↑((n + 1) * n !)) *
      (↑(2 * n)! ^ 0 * ↑(2 * n)! * ↑(2 * n)! * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Proof state:
case zero

⊢ 1 = 1 * ↑1 ^ 4 / (↑1 ^ 2 * (2 * ↑0 + 1))

Tactic:
norm_num

Result:
no goals

Proof state:
case zero

⊢ W 0 = 2 ^ (4 * 0) * ↑0! ^ 4 / (↑(2 * 0)! ^ 2 * (2 * ↑0 + 1))

Tactic:
simp only [W, prod_range_zero, Nat.factorial_zero, mul_zero, pow_zero,
  algebraMap.coe_one, one_pow, mul_one, algebraMap.coe_zero, zero_add, div_self, Ne,
  one_ne_zero, not_false_iff]

Result:
case zero

⊢ 1 = 1 * ↑1 ^ 4 / (↑1 ^ 2 * (2 * ↑0 + 1))

Proof state:
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 0 < ↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1)

Tactic:
positivity

Result:
no goals

Proof state:
case succ.refine_1
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)) ≠ 0

case succ.refine_2
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1) ≠ 0

case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 * (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Tactic:
any_goals exact ne_of_gt (by positivity)

Result:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 * (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Proof state:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) /
      (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3))) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Tactic:
refine (div_eq_div_iff ?_ ?_).mpr ?_

Result:
case succ.refine_1
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)) ≠ 0

case succ.refine_2
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1) ≠ 0

case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n + 2) * (2 * ↑n + 2)) * (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 * (↑(2 * n)! ^ 2 * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Proof state:
case succ
n : ℕ
IH : W n = 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ W (n + 1) = 2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Tactic:
unfold W at IH ⊢

Result:
case succ
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ ∏ i ∈ range (n + 1), (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * (n + 1)) * ↑(n + 1)! ^ 4 / (↑(2 * (n + 1))! ^ 2 * (2 * ↑(n + 1) + 1))

Proof state:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! ^ 0 * ↑n ! * ↑n ! * ↑n ! * ↑n !) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) ^ 0 * ↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) *
          ↑((2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!)) *
        (2 * ↑(n + 1) + 1)) =
    2 ^ (4 * n) * 2 * 2 * 2 * 2 *
        (↑((n + 1) * n !) ^ 0 * ↑((n + 1) * n !) * ↑((n + 1) * n !) * ↑((n + 1) * n !) * ↑((n + 1) * n !)) *
      (↑(2 * n)! ^ 0 * ↑(2 * n)! * ↑(2 * n)! * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))

Tactic:
push_cast

Result:
case succ.refine_3
n : ℕ
IH :
  ∏ i ∈ range n, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3)) =
    2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
⊢ 2 ^ (4 * n) * (↑n ! ^ 0 * ↑n ! * ↑n ! * ↑n ! * ↑n !) * ((2 * ↑n + 2) * (2 * ↑n + 2)) *
      (((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) ^ 0 * ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
          ((2 * ↑n + 1 + 1) * ((2 * ↑n + 1) * ↑(2 * n)!)) *
        (2 * (↑n + 1) + 1)) =
    2 ^ (4 * n) * 2 * 2 * 2 * 2 *
        (((↑n + 1) * ↑n !) ^ 0 * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !) * ((↑n + 1) * ↑n !)) *
      (↑(2 * n)! ^ 0 * ↑(2 * n)! * ↑(2 * n)! * (2 * ↑n + 1) * ((2 * ↑n + 1) * (2 * ↑n + 3)))