a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
⊢ (∫ (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)
a b : ℝ
n : ℕ
⊢ (∫ (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)
have continuous_sin_pow : ∀ (k : ℕ), (Continuous fun x => sin x ^ k) :=
  fun k => continuous_sin.pow k
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
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)
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
⊢ (∫ (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)
let C := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
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)
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
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)
have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), 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)
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
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)
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)
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) 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)
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), 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)
have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x := fun x _ => by
  simpa only [neg_neg] using (hasDerivAt_cos x).neg
case refine_3
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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)

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

case refine_2
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => sin x) MeasureTheory.volume a b
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) 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)
have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
case refine_1.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => ↑(n + 1) * cos x * sin x ^ n

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

case refine_2
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => sin x) MeasureTheory.volume a b
all_goals apply Continuous.intervalIntegrable
no goals
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
α β γ : ℝ
⊢ β * α * γ * α = β * (α * α * γ)
ring
no goals
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
simpa only [mul_right_comm] using (hasDerivAt_sin x).pow (n + 1)
no goals
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), 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
simpa only [neg_neg] using (hasDerivAt_cos x).neg
no goals
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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)) = ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x
simp only [_root_.pow_succ']
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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 = sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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 + 1) * sin x) = C + (↑n + ↑1) * ∫ (x : ℝ) in a..b, cos x ^ 2 * sin x ^ n
simp [H, h, sq]
no goals
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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 = sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
ring
no goals
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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)
simp [cos_sq', sub_mul, ← pow_add, add_comm]
case hf.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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
⊢ Continuous fun x => sin x ^ n

case hg.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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
⊢ Continuous fun x => sin x ^ (n + 2)
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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)
rw [integral_sub, mul_sub, add_sub_assoc] <;> apply Continuous.intervalIntegrable
no goals
case hf.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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
⊢ Continuous fun x => sin x ^ n
exact continuous_sin_pow n
no goals
case hg.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), 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
⊢ Continuous fun x => sin x ^ (n + 2)
exact continuous_sin_pow (n + 2)
case refine_2.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => sin x
case refine_2
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ IntervalIntegrable (fun x => sin x) MeasureTheory.volume a b
apply Continuous.intervalIntegrable
case refine_1.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
this : Continuous fun x => ↑(n + 1) * cos x
⊢ Continuous fun x => ↑(n + 1) * cos x * sin x ^ n
case refine_1.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => ↑(n + 1) * cos x * sin x ^ n
have : Continuous fun x ↦ ↑(n + 1) * cos x := by continuity
no goals
case refine_1.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
this : Continuous fun x => ↑(n + 1) * cos x
⊢ Continuous fun x => ↑(n + 1) * cos x * sin x ^ n
exact this.mul (continuous_sin_pow n)
no goals
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => ↑(n + 1) * cos x
continuity
no goals
case refine_2.hu
a b : ℝ
n : ℕ
continuous_sin_pow : ∀ (k : ℕ), Continuous fun x => sin x ^ k
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (fun y => sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt (-cos) (sin x) x
⊢ Continuous fun x => sin x
exact continuous_sin