case zero
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * zero)) = π * ∏ i in Finset.range zero, (2 * ↑i + 1) / (2 * ↑i + 2)

case succ
a b : ℝ
n k : ℕ
ih : (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * succ k)) = π * ∏ i in Finset.range (succ k), (2 * ↑i + 1) / (2 * ↑i + 2)
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * n)) = π * ∏ i in Finset.range n, (2 * ↑i + 1) / (2 * ↑i + 2)
induction' n with k ih
case succ
a b : ℝ
n k : ℕ
ih : (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ((sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
case succ
a b : ℝ
n k : ℕ
ih : (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * succ k)) = π * ∏ i in Finset.range (succ k), (2 * ↑i + 1) / (2 * ↑i + 2)
rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
case succ
a b : ℝ
n k : ℕ
ih : (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ((sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / ↑(2 * k + 2) +
      ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
case succ
a b : ℝ
n k : ℕ
ih : (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ((sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
norm_cast
no goals
case succ
a b : ℝ
n k : ℕ
ih : (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) = π * ∏ i in Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ((sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / ↑(2 * k + 2) +
      ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)) =
    ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
simp [-cast_add, field_simps]
no goals
case zero
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (2 * zero)) = π * ∏ i in Finset.range zero, (2 * ↑i + 1) / (2 * ↑i + 2)
simp