a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, sin x ^ (2 * 0 + 1) * cos x ^ 2) = ∫ (u : ℝ) in cos b..cos a, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ (∫ (x : ℝ) in a..b, sin x * cos x ^ 2) = (cos a ^ 3 - cos b ^ 3) / 3
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x * cos x ^ 2) = (cos a ^ 3 - cos b ^ 3) / 3
have := @integral_sin_pow_odd_mul_cos_pow a b 0 2
a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, sin x * cos x ^ 2) = (cos a ^ 3 - cos b ^ 3) / 3
⊢ (∫ (x : ℝ) in a..b, sin x * cos x ^ 2) = (cos a ^ 3 - cos b ^ 3) / 3
a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, sin x ^ (2 * 0 + 1) * cos x ^ 2) = ∫ (u : ℝ) in cos b..cos a, u ^ 2 * (1 - u ^ 2) ^ 0
⊢ (∫ (x : ℝ) in a..b, sin x * cos x ^ 2) = (cos a ^ 3 - cos b ^ 3) / 3
norm_num at this
no goals
a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, sin x * cos x ^ 2) = (cos a ^ 3 - cos b ^ 3) / 3
⊢ (∫ (x : ℝ) in a..b, sin x * cos x ^ 2) = (cos a ^ 3 - cos b ^ 3) / 3
exact this