no goals
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (∫ (x : ℝ) in a..b, sin x ^ (2 * m + 1) * cos x ^ n) = -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n
rw [integral_symm]
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n) =
    ∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (-∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n) = ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n
simp only [_root_.pow_succ', pow_mul, _root_.pow_zero, one_mul, mul_neg, neg_mul,
  integral_neg, neg_inj]
case h.e'_5.h.h.e'_5.h.e'_5.h.e'_5
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ * sin x✝ = 1 - cos x✝ * cos x✝
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n) =
    ∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n
congr! 5
no goals
case h.e'_5.h.h.e'_5.h.e'_5.h.e'_5
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ * sin x✝ = 1 - cos x✝ * cos x✝
rw [← sq, ← sq, sin_sq]
case e_f
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (fun x => (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n) = fun x => cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n) =
    ∫ (x : ℝ) in b..a, cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x
congr
case e_f.h
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ (1 - cos x✝ ^ 2) ^ m * -sin x✝ * cos x✝ ^ n = cos x✝ ^ n * (1 - cos x✝ ^ 2) ^ m * -sin x✝
case e_f
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (fun x => (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n) = fun x => cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x
ext
no goals
case e_f.h
a b : ℝ
n✝ m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ (1 - cos x✝ ^ 2) ^ m * -sin x✝ * cos x✝ ^ n = cos x✝ ^ n * (1 - cos x✝ ^ 2) ^ m * -sin x✝
ring