awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -(↑(n + 1) : ℝ) * sin x * cos x ^ n * sin x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
have x : Eq (α := ℝ) (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) (∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x)
Tactic: calc
      (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by
        simp only [_root_.pow_succ]
      _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [C, H, h, sq, -neg_add_rev]
      _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by
        simp [sin_sq, sub_mul, ← pow_add, add_comm]
      _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos 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 : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -(↑(n + 1) : ℝ) * sin x * cos x ^ n * sin x
x : Eq (α := ℝ) (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) (∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x)
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
have x₁ : ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
  C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x ^ n
Tactic: calc
      (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by
        simp only [_root_.pow_succ]
      _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [C, H, h, sq, -neg_add_rev]
      _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by
        simp [sin_sq, sub_mul, ← pow_add, add_comm]
      _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos 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 : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -(↑(n + 1) : ℝ) * sin x * cos x ^ n * sin x
x : Eq (α := ℝ) (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) (∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x)
x₁ :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x ^ n
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
have x₂ : C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x ^ n =
  C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n - cos x ^ (n + 2)
Tactic: calc
      (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by
        simp only [_root_.pow_succ]
      _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [C, H, h, sq, -neg_add_rev]
      _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by
        simp [sin_sq, sub_mul, ← pow_add, add_comm]
      _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos 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 : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -(↑(n + 1) : ℝ) * sin x * cos x ^ n * sin x
x : Eq (α := ℝ) (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) (∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x)
x₁ :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x ^ n
x₂ :
  C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x ^ n =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n - cos x ^ (n + 2)
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n) -
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
have x₃ : C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n - cos x ^ (n + 2) =
  (C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n) -
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
Tactic: calc
      (∫ x in a..b, cos x ^ (n + 2)) = ∫ x in a..b, cos x ^ (n + 1) * cos x := by
        simp only [_root_.pow_succ]
      _ = C + (n + 1) * ∫ x in a..b, sin x ^ 2 * cos x ^ n := by simp [C, H, h, sq, -neg_add_rev]
      _ = C + (n + 1) * ∫ x in a..b, cos x ^ n - cos x ^ (n + 2) := by
        simp [sin_sq, sub_mul, ← pow_add, add_comm]
      _ = (C + (n + 1) * ∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos 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 : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ -(↑(n + 1) : ℝ) * sin x * cos x ^ n) MeasureTheory.volume a b
have refine_1 : Continuous (Y := ℝ) fun (x : ℝ) ↦ -(↑(n + 1) : ℝ) * sin x * cos x ^ n
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable cos MeasureTheory.volume a b
have refine_2 : Continuous cos
Tactic: apply Continuous.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * ∫ (x : ℝ) in a..b, cos x ^ n
have field_simp : (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 =
  cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ n
have h : (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 =
  (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
Tactic: convert! eq_sub_iff_add_eq.mp (integral_cos_pow_aux n) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ m * cos x ^ (2 * n + 1))
    (∫ (x : ℝ) in a..b, sin x ^ m * (1 - HPow.hPow (β := ℕ) (sin x) 2) ^ n * cos x)
have simp : Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ m * ((cos x * cos x) ^ n * cos x))
  (∫ (x : ℝ) in a..b, sin x ^ m * ((1 - sin x * sin x) ^ n * cos x))
Tactic: simp only [_root_.pow_zero, _root_.pow_succ, mul_assoc, pow_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ m * ((cos x * cos x) ^ n * cos x))
    (∫ (x : ℝ) in a..b, sin x ^ m * ((1 - sin x * sin x) ^ n * cos x))
have h : ∀ (x : ℝ), cos x * cos x = 1 - sin x * sin x
Tactic: congr! 5
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n
x : ℝ
⊢ cos x * cos x = 1 - sin x * sin x
have h : HPow.hPow (β := ℕ) (cos x) 2 = 1 - sin x * sin x
Tactic: rw [← sq, ← sq, cos_sq']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n
x : ℝ
h : HPow.hPow (β := ℕ) (cos x) 2 = 1 - sin x * sin x
⊢ cos x * cos x = 1 - sin x * sin x
have h₁ : HPow.hPow (β := ℕ) (cos x) 2 = 1 - HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [← sq, ← sq, cos_sq']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n
x : ℝ
h : HPow.hPow (β := ℕ) (cos x) 2 = 1 - sin x * sin x
h₁ : HPow.hPow (β := ℕ) (cos x) 2 = 1 - HPow.hPow (β := ℕ) (sin x) 2
⊢ cos x * cos x = 1 - sin x * sin x
have h₂ : 1 - HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [← sq, ← sq, cos_sq']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x =
    (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3
have this : Eq (α := ℝ) (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x ^ (HMul.hMul (α := ℕ) 2 0 + 1))
  (∫ (u : ℝ) in sin a..sin b, HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) u 2) 0)
Tactic: have := @integral_sin_pow_mul_cos_pow_odd a b 2 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 3 =
    sin b - sin a - (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3
have this : Eq (α := ℝ) (∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 0 * cos x ^ (HMul.hMul (α := ℕ) 2 1 + 1))
  (∫ (u : ℝ) in sin a..sin b, HPow.hPow (β := ℕ) u 0 * HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) u 2) 1)
Tactic: have := @integral_sin_pow_mul_cos_pow_odd a b 0 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (2 * m + 1) * cos x ^ n) (-∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n)
have rw : Eq (α := ℝ) (-∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n) (-∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n)
Tactic: rw [integral_symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
⊢ Eq (α := ℝ) (-∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n)
    (∫ (x : ℝ) in b..a, (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x * cos x ^ n)
have simp : Eq (α := ℝ) (∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n)
  (∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n)
Tactic: simp only [_root_.pow_succ, pow_mul, _root_.pow_zero, one_mul, mul_neg, neg_mul,
        integral_neg, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
⊢ Eq (α := ℝ) (∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n)
    (∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n)
have h : ∀ (x : ℝ), sin x * sin x = 1 - cos x * cos x
Tactic: congr! 5
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
x : ℝ
⊢ sin x * sin x = 1 - cos x * cos x
have h : HPow.hPow (β := ℕ) (sin x) 2 = 1 - cos x * cos x
Tactic: rw [← sq, ← sq, sin_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
x : ℝ
h : HPow.hPow (β := ℕ) (sin x) 2 = 1 - cos x * cos x
⊢ sin x * sin x = 1 - cos x * cos x
have h₁ : HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sq, ← sq, sin_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
x : ℝ
h : HPow.hPow (β := ℕ) (sin x) 2 = 1 - cos x * cos x
h₁ : HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2
⊢ sin x * sin x = 1 - cos x * cos x
have h₂ : 1 - HPow.hPow (β := ℕ) (cos x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sq, ← sq, sin_sq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
⊢ Eq (α := ℝ) (∫ (x : ℝ) in b..a, (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x * cos x ^ n)
    (∫ (x : ℝ) in b..a, cos x ^ n * (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x)
have e_f : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x * cos x ^ n) fun (x : ℝ) ↦
  cos x ^ n * (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x * cos x ^ n) fun (x : ℝ) ↦
    cos x ^ n * (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x
have e_f : ∀ (x : ℝ),
  (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x * cos x ^ n =
    cos x ^ n * (1 - HPow.hPow (β := ℕ) (cos x) 2) ^ m * -sin x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * HPow.hPow (β := ℕ) (cos x) 2 =
    (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3
have this : Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (HMul.hMul (α := ℕ) 2 0 + 1) * HPow.hPow (β := ℕ) (cos x) 2)
  (∫ (u : ℝ) in cos b..cos a, HPow.hPow (β := ℕ) u 2 * HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) u 2) 0)
Tactic: have := @integral_sin_pow_odd_mul_cos_pow a b 0 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 3 =
    cos a - cos b - (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3
have this : Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (HMul.hMul (α := ℕ) 2 1 + 1) * HPow.hPow (β := ℕ) (cos x) 0)
  (∫ (u : ℝ) in cos b..cos a, HPow.hPow (β := ℕ) u 0 * HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) u 2) 1)
Tactic: have := @integral_sin_pow_odd_mul_cos_pow a b 1 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, sin x ^ (2 * m) * cos x ^ (2 * n))
    (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
have simp : Eq (α := ℝ) (∫ (x : ℝ) in a..b, (HSub.hSub (α := ℝ) 1 2⁻¹ - cos (2 * x) / 2) ^ m * (2⁻¹ + cos (2 * x) / 2) ^ n)
  (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
Tactic: simp [pow_mul, sin_sq, cos_sq, ← sub_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
m n : ℕ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (HSub.hSub (α := ℝ) 1 2⁻¹ - cos (2 * x) / 2) ^ m * (2⁻¹ + cos (2 * x) / 2) ^ n)
    (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
have field_simp : Eq (α := ℝ) (∫ (x : ℝ) in a..b, ((HSub.hSub (α := ℝ) 2 1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
  (∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * HPow.hPow (β := ℕ) (cos x) 2 =
    (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32
have h : (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1
Tactic: convert! integral_sin_pow_even_mul_cos_pow_even 1 1 using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1
have h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
Tactic: have h1 : ∀ c : ℝ, (↑1 - c) / ↑2 * ((↑1 + c) / ↑2) = (↑1 - c ^ 2) / 4 := fun c => by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1
have h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
Tactic: have h2 : Continuous fun x => cos (2 * x) ^ 2 := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
x : ℝ
⊢ cos x * sin x = sin (2 * x) / 2
have rw : cos x * sin x = 2 * sin x * cos x / 2
Tactic: rw [sin_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1
have h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
Tactic: have h3 : ∀ x, cos x * sin x = sin (2 * x) / 2 := by intro; rw [sin_two_mul]; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1
have h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
Tactic: have h4 : ∀ d : ℝ, 2 * (2 * d) = 4 * d := fun d => by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - HPow.hPow (β := ℕ) c 2) / 4
h2 : Continuous (Y := ℝ) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (cos (2 * x)) 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) ((1 - cos (2 * x)) / 2) 1 * HPow.hPow (β := ℕ) ((1 + cos (2 * x)) / 2) 1
have h : (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
  (b - a - 2⁻¹ * ((sin (4 * b) / 2 - sin (4 * a) / 2 + 2 * b - 2 * a) / 2)) / 4
Tactic: simp [h1, h2.intervalIntegrable, integral_comp_mul_left fun x => cos x ^ 2, h3, h4]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
    (∫ (x : ℝ) in sin (-(π / 2))..sin (π / 2), √(1 - HPow.hPow (β := ℕ) x 2))
have rw : Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
  (∫ (x : ℝ) in -sin (π / 2)..sin (π / 2), √(1 - HPow.hPow (β := ℕ) x 2))
Tactic: rw [sin_neg, sin_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
    (∫ (x : ℝ) in -sin (π / 2)..sin (π / 2), √(1 - HPow.hPow (β := ℕ) x 2))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
    (∫ (x : ℝ) in sin (-(π / 2))..sin (π / 2), √(1 - HPow.hPow (β := ℕ) x 2))
have rw₁ : Eq (α := ℝ) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2)) (∫ (x : ℝ) in -1..1, √(1 - HPow.hPow (β := ℕ) x 2))
Tactic: rw [sin_neg, sin_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x)
    (∫ (x : ℝ) in -(π / 2)..π / 2, HPow.hPow (β := ℕ) (cos x) 2)
have refine : ∀ (x : ℝ) (h : x ∈ Ι (-(π / 2)) (π / 2)), √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x = HPow.hPow (β := ℕ) (cos x) 2
Tactic: refine integral_congr_ae (MeasureTheory.ae_of_all _ fun _ h => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
x : ℝ
h : x ∈ Ι (-(π / 2)) (π / 2)
⊢ √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x = HPow.hPow (β := ℕ) (cos x) 2
have h₁ : -(π / 2) < x ∧ x ≤ π / 2
Tactic: rw [uIoc_of_le (neg_le_self (le_of_lt (half_pos Real.pi_pos))), Set.mem_Ioc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
x : ℝ
h : -(π / 2) < x ∧ x ≤ π / 2
⊢ √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x = HPow.hPow (β := ℕ) (cos x) 2
have rw : cos x * cos x = HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← Real.cos_eq_sqrt_one_sub_sin_sq (le_of_lt h.1) h.2, pow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
x : ℝ
h : -(π / 2) < x ∧ x ≤ π / 2
rw : cos x * cos x = HPow.hPow (β := ℕ) (cos x) 2
⊢ √(1 - HPow.hPow (β := ℕ) (sin x) 2) * cos x = HPow.hPow (β := ℕ) (cos x) 2
have rw₁ : cos x * cos x = cos x * cos x
Tactic: rw [← Real.cos_eq_sqrt_one_sub_sin_sq (le_of_lt h.1) h.2, pow_two]