n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼
n : ℕ
⊢ (2 * (n + 1) + 1)‼ = ∏ i in Finset.range (n + 1), (2 * (i + 1) + 1)
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
  (by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]
no goals
n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼
rfl
no goals
n : ℕ
⊢ 2 * (n + 1) + 1 = 2 * n + 1 + 2
ring