awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
h :
  (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
⊢ (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) -
          (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
      ℂ)
have h₁ : (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
    ℂ) =
  (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
    (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
Tactic: convert! integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
h :
  (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
h₁ :
  (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
      ℂ) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
convert_1 convert_2 : ℝ
⊢ (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) -
          (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
      ℂ)
have convert_3 : (↑t : ℂ) ≠ -1
Tactic: convert! integral_mul_cpow_one_add_sq (_ : (t : ℂ) ≠ -1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ (↑(∫ (x : ℝ) in a..b, x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) =
    ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
have h : Eq (α := ℂ) (∫ (x : ℝ) in a..b, (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ))
  (∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ))
Tactic: rw [← intervalIntegral.integral_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ Eq (α := ℂ) (∫ (x : ℝ) in a..b, (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ))
    (∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ))
have h : ∀ (x : ℝ), (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
Tactic: congr with x : 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
x : ℝ
⊢ (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
have h : (↑x : ℂ) * (↑((1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
Tactic: rw [ofReal_mul, this x t]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
x : ℝ
h : (↑x : ℂ) * (↑((1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
⊢ (↑(x * (1 + HPow.hPow (β := ℕ) x 2) ^ t) : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
have h₁ : (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ) = (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑t : ℂ)
Tactic: rw [ofReal_mul, this x t]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ (↑((1 + HPow.hPow (β := ℕ) b 2) ^ (t + 1) / (2 * (t + 1)) - (1 + HPow.hPow (β := ℕ) a 2) ^ (t + 1) / (2 * (t + 1))) :
      ℂ) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
have h : (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) -
    (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) =
  (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
    (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
Tactic: simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (↑(t + 1) : ℂ) / (↑(2 * (t + 1)) : ℂ) =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
have h : (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
    (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) =
  (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1)) -
    (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ ((↑t : ℂ) + 1) / (2 * ((↑t : ℂ) + 1))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), (↑((1 + HPow.hPow (β := ℕ) x 2) ^ s) : ℂ) = (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ (↑s : ℂ)
⊢ (↑t : ℂ) ≠ -1
have convert_3 : ¬t = -1
Tactic: rw [← ofReal_one, ← ofReal_neg, Ne, ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
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 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
Tactic: have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
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 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑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
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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
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 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
Tactic: have hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x := fun x _ => by
    simpa only [neg_neg] using (hasDerivAt_cos x).neg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have refine_3 : ∀
  (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 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
Tactic: have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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
refine_3 :
  ∀
    (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 +
          HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
        HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have refine_1 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑(n + 1) : ℝ) * cos x * sin x ^ n) MeasureTheory.volume a b
Tactic: have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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
refine_3 :
  ∀
    (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 +
          HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
        HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
refine_1 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑(n + 1) : ℝ) * cos x * sin x ^ n) MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have refine_2 : IntervalIntegrable sin MeasureTheory.volume a b
Tactic: have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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 + 1) * sin x =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n
have simp : -(sin b ^ (n + 1) * cos b) + sin a ^ (n + 1) * cos a = C
Tactic: simp [H, h, sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2) =
    (C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume a b
Tactic: rw [integral_sub, mul_sub, add_sub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume a b
⊢ C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2) =
    (C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ (n + 2)) MeasureTheory.volume a b
Tactic: rw [integral_sub, mul_sub, add_sub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume a b
have hf : Continuous (Y := ℝ) fun (x : ℝ) ↦ sin x ^ n
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ (n + 2)) MeasureTheory.volume a b
have hg : Continuous (Y := ℝ) fun (x : ℝ) ↦ sin x ^ (n + 2)
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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 + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have x : Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) (∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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 : Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) (∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x)
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have x₁ : ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
  C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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 : Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) (∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x)
x₁ :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have x₂ : C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n =
  C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n - 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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 : Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) (∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x)
x₁ :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n
x₂ :
  C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 * sin x ^ n =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2)
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
have x₃ : C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n - sin x ^ (n + 2) =
  (C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ n) -
    HAdd.hAdd (α := ℝ) (↑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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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 (ε := ℝ) (fun (x : ℝ) ↦ (↑(n + 1) : ℝ) * cos x * sin x ^ n) MeasureTheory.volume a b
have refine_1 : Continuous (Y := ℝ) fun (x : ℝ) ↦ (↑(n + 1) : ℝ) * cos x * sin x ^ n
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
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
have refine_2 : Continuous sin
Tactic: apply Continuous.intervalIntegrable