n : ℕ
⊢ (2 * n + 2) * (2 ^ n * n !) = 2 ^ n * 2 * ((n + 1) * n !)
n : ℕ
⊢ (2 * (n + 1))‼ = 2 ^ (n + 1) * (n + 1)!
rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _,
  succ_eq_add_one]
no goals
n : ℕ
⊢ (2 * n + 2) * (2 ^ n * n !) = 2 ^ n * 2 * ((n + 1) * n !)
ring