awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
x : ℝ
h_1 : x ∈ [[a, b]]
⊢ HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x

Tactic:
simpa only [mul_right_comm, neg_mul, mul_neg] using (hasDerivAt_cos x).pow (n + 1)

Premises used: HasDerivAt.pow, Real.hasDerivAt_cos, HAdd.hAdd, mul_right_comm, neg_mul, OfNat.ofNat, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun (y : ℝ) ↦ cos y ^ (n + 1)) (-(↑(n + 1) : ℝ) * sin x * cos x ^ n) x

Tactic:
have hu : ∀ x ∈ [[a, b]],
      HasDerivAt (fun y => cos y ^ (n + 1)) (-(n + 1 : ℕ) * sin x * cos x ^ n) x :=
    fun x _ => by
      simpa only [mul_right_comm, neg_mul, mul_neg] using (hasDerivAt_cos x).pow (n + 1)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x

Tactic:
have hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x := fun x _ => hasDerivAt_sin x
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
refine_3 :
  ∀
    (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)
refine_1 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ -(↑(n + 1) : ℝ) * sin x * cos x ^ n) MeasureTheory.volume a b
refine_2 : IntervalIntegrable cos MeasureTheory.volume a b
⊢ ∫ (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)

Tactic:
have H := integral_mul_deriv_eq_deriv_mul hu hv ?_ ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) (∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x)

Tactic:
simp only [_root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 + 1) * cos x =
    C + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x ^ n

Tactic:
simp [C, H, h, sq, -neg_add_rev]

Premises used: neg_add_rev, sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ 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:
simp [sin_sq, sub_mul, ← pow_add, add_comm]

Premises used: Real.sin_sq, pow_add, add_comm, sub_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos x ^ n) MeasureTheory.volume a b
hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos x ^ (n + 2)) MeasureTheory.volume a b
⊢ 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:
rw [integral_sub, mul_sub, add_sub_assoc]

Premises used: add_sub_assoc, mul_sub, intervalIntegral.integral_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
hf : Continuous (Y := ℝ) fun (x : ℝ) ↦ cos x ^ n
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos x ^ n) MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
hg : Continuous (Y := ℝ) fun (x : ℝ) ↦ cos x ^ (n + 2)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos x ^ (n + 2)) MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ cos x ^ n

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ cos x ^ (n + 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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₃ :
  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)
⊢ ∫ (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)

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

Premises used: HMul.hMul, Real.cos, intervalIntegral, Nat.cast, HPow.hPow, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
refine_1 : Continuous (Y := ℝ) fun (x : ℝ) ↦ -(↑(n + 1) : ℝ) * sin x * cos x ^ n
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ -(↑(n + 1) : ℝ) * sin x * cos x ^ n) MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ -(↑(n + 1) : ℝ) * sin x * cos x ^ n

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
refine_2 : Continuous cos
⊢ IntervalIntegrable cos MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
⊢ Continuous cos

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
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
⊢ ∫ (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

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (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

Tactic:
eq_sub_iff_add_eq.mp (integral_cos_pow_aux n)

Premises used: integral_cos_pow_aux, eq_sub_iff_add_eq, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
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)
⊢ (∫ (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:
convert! eq_sub_iff_add_eq.mp (integral_cos_pow_aux n) using 1

Premises used: integral_cos_pow_aux, eq_sub_iff_add_eq, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
⊢ (∫ (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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 = (cos b * sin b - cos a * sin a + b - a) / 2

Tactic:
simp [field, integral_cos_pow, add_sub_assoc]

Premises used: add_sub_assoc, integral_cos_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
⊢ Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n
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))
⊢ 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)

Tactic:
simp only [_root_.pow_zero, _root_.pow_succ, mul_assoc, pow_mul, one_mul]

Premises used: pow_succ, mul_assoc, pow_mul, pow_zero, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ m * (1 - HPow.hPow (β := ℕ) u 2) ^ n
h : ∀ (x : ℝ), cos x * cos x = 1 - sin x * sin x
⊢ 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:
congr! 5
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
h₂ h₃ : 1 - HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (sin x) 2
⊢ cos x * cos x = 1 - sin x * sin x

Tactic:
rw [← sq, ← sq, cos_sq']

Premises used: sq, Real.cos_sq'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x = (HPow.hPow (β := ℕ) (sin b) 2 - HPow.hPow (β := ℕ) (sin a) 2) / 2

Tactic:
simpa using integral_sin_pow_mul_cos_pow_odd 1 0

Premises used: integral_sin_pow_mul_cos_pow_odd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
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)
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x =
    (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3

Tactic:
norm_num at this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x =
    (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x =
    (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x =
    (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (sin x) 2 * cos x =
    (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
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)
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 3 =
    sin b - sin a - (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3

Tactic:
norm_num at this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 3 =
    sin b - sin a - (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 3 =
    sin b - sin a - (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
this :
  ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 3 =
    sin b - sin a - (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 3 =
    sin b - sin a - (HPow.hPow (β := ℕ) (sin b) 3 - HPow.hPow (β := ℕ) (sin a) 3) / 3

Tactic:
exact this
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
⊢ Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
rw 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)
⊢ 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)

Tactic:
rw [integral_symm]

Premises used: intervalIntegral.integral_symm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
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)
⊢ 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)

Tactic:
simp only [_root_.pow_succ, pow_mul, _root_.pow_zero, one_mul, mul_neg, neg_mul,
        integral_neg, neg_inj]

Premises used: pow_succ, pow_mul, pow_zero, neg_inj, neg_mul, intervalIntegral.integral_neg, one_mul, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
h : ∀ (x : ℝ), sin x * sin x = 1 - cos x * cos x
⊢ 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:
congr! 5
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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
h₂ h₃ : 1 - HPow.hPow (β := ℕ) (cos x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2
⊢ sin x * sin x = 1 - cos x * cos x

Tactic:
rw [← sq, ← sq, sin_sq]

Premises used: Real.sin_sq, sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
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
⊢ 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)

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
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
⊢ 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:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
m n : ℕ
hc : Continuous (Y := ℝ) fun (u : ℝ) ↦ u ^ n * (1 - HPow.hPow (β := ℕ) u 2) ^ m
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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x = (HPow.hPow (β := ℕ) (cos a) 2 - HPow.hPow (β := ℕ) (cos b) 2) / 2

Tactic:
simpa using integral_sin_pow_odd_mul_cos_pow 0 1

Premises used: integral_sin_pow_odd_mul_cos_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
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)
⊢ ∫ (x : ℝ) in a..b, sin x * HPow.hPow (β := ℕ) (cos x) 2 =
    (HPow.hPow (β := ℕ) (cos a) 3 - HPow.hPow (β := ℕ) (cos b) 3) / 3

Tactic:
norm_num at this