a b : ℝ
n : ℕ
this : n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
have : n + 2 ≠ 0 := by linarith
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
a b : ℝ
n : ℕ
this : n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
have : (n : ℝ) + 2 ≠ 0 := by norm_cast
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n
field_simp
case h.e'_2
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n
convert eq_sub_iff_add_eq.mp (integral_sin_pow_aux n) using 1
no goals
case h.e'_2
a b : ℝ
n : ℕ
this✝ : n + 2 ≠ 0
this : ↑n + 2 ≠ 0
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
ring
no goals
a b : ℝ
n : ℕ
⊢ n + 2 ≠ 0
linarith
no goals
a b : ℝ
n : ℕ
this : n + 2 ≠ 0
⊢ ↑n + 2 ≠ 0
norm_cast