no goals
a b : ℝ
n✝ m n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (2 * m) * cos x ^ (2 * n)) =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n
field_simp [pow_mul, sin_sq, cos_sq, ← sub_sub, (by ring : (2 : ℝ) - 1 = 1)]
no goals
a b : ℝ
n✝ m n : ℕ
⊢ 2 - 1 = 1
ring