[GOAL]
n : ℕ
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ (zero + 1)‼ = (zero + 1) * (zero - 1)‼
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ (succ n✝ + 1)‼ = (succ n✝ + 1) * (succ n✝ - 1)‼
[PROOFSTEP]
rfl
[GOAL]
k : ℕ
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
[PROOFSTEP]
rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼, mul_assoc]
[GOAL]
n : ℕ
⊢ (2 * (n + 1))‼ = 2 ^ (n + 1) * (n + 1)!
[PROOFSTEP]
rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _, succ_eq_add_one]
[GOAL]
n : ℕ
⊢ (2 * n + 2) * (2 ^ n * n !) = 2 ^ n * 2 * ((n + 1) * n !)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (2 * (n + 1))‼ = ∏ i in Finset.range (n + 1), 2 * (i + 1)
[PROOFSTEP]
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_even _, mul_comm (2 * n)‼, (by ring : 2 * (n + 1) = 2 * n + 2)]
[GOAL]
n : ℕ
⊢ 2 * (n + 1) = 2 * n + 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ (2 * (n + 1) + 1)‼ = ∏ i in Finset.range (n + 1), (2 * (i + 1) + 1)
[PROOFSTEP]
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
  (by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]
[GOAL]
n : ℕ
⊢ 2 * (n + 1) + 1 = 2 * n + 1 + 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼
[PROOFSTEP]
rfl
