-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_aux :
    (∫ x in a..b, sin x ^ (n + 2)) =
      (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ x in a..b, sin x ^ n) -
        (↑n + 1) * ∫ x in a..b, sin x ^ (n + 2)

Proof state:
case refine_2
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable sin MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable

Result:
case refine_2.hu
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
⊢ Continuous sin

Proof state:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring

Result:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Proof state:
case refine_2.hu
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
⊢ Continuous sin

Tactic:
fun_prop

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ 2 * sin x ^ n =
    C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2)

Tactic:
simp [cos_sq', sub_mul, ← pow_add, add_comm]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ -(sin b ^ (n + 1) * cos b) + sin a ^ (n + 1) * cos a = C

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
have hu : ∀ x ∈ [[a, b]],
    HasDerivAt (fun y => sin y ^ (n + 1)) ((n + 1 : ℕ) * cos x * sin x ^ n) x :=
  fun x _ => by simpa only [mul_right_comm] using (hasDerivAt_sin x).pow (n + 1)

Result:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Proof state:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
α β γ : ℝ
⊢ β * α * γ * α = β * (α * α * γ)

Tactic:
ring

Result:
no goals

Proof state:
case refine_3
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
calc
  (∫ x in a..b, sin x ^ (n + 2)) = ∫ x in a..b, sin x ^ (n + 1) * sin x := by
    simp only [_root_.pow_succ]
  _ = C + (↑n + 1) * ∫ x in a..b, cos x ^ 2 * sin x ^ n := by simp [H, h, sq]; ring
  _ = C + (↑n + 1) * ∫ x in a..b, sin x ^ n - sin x ^ (n + 2) := by
    simp [cos_sq', sub_mul, ← pow_add, add_comm]
  _ = (C + (↑n + 1) * ∫ x in a..b, sin x ^ n) - (↑n + 1) * ∫ x in a..b, sin x ^ (n + 2) := by
    rw [integral_sub, mul_sub, add_sub_assoc] <;>
      apply Continuous.intervalIntegrable <;> fun_prop

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (-cos) (sin x) x

Tactic:
simpa only [neg_neg] using (hasDerivAt_cos x).neg

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2) =
    (C + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
rw [integral_sub, mul_sub, add_sub_assoc] <;>
  apply Continuous.intervalIntegrable <;> fun_prop

Result:
no goals