awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
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 : Continuous (Y := ℝ) fun (x : ℝ) ↦ sin x ^ n
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin 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 : ℝ := 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
hg : Continuous (Y := ℝ) fun (x : ℝ) ↦ sin x ^ (n + 2)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin 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 : ℝ := 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
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ sin x ^ n

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

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

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

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

Tactic:
apply Continuous.intervalIntegrable

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

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

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

Tactic:
eq_sub_iff_add_eq.mp (integral_sin_pow_aux n)

Premises used: eq_sub_iff_add_eq, integral_sin_pow_aux, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
h :
  (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 =
    (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * HAdd.hAdd (α := ℝ) (↑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

Tactic:
convert! eq_sub_iff_add_eq.mp (integral_sin_pow_aux n) using 1

Premises used: eq_sub_iff_add_eq, integral_sin_pow_aux, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 =
    (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

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

Tactic:
simp [field, integral_sin_pow, add_sub_assoc]

Premises used: add_sub_assoc, integral_sin_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (HMul.hMul (α := ℕ) 2 0 + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range 0, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
succ :
  (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * k + 1) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * k + 1) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * k + 1) : ℝ) 2 *
        ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1) + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range (k + 1), (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))

Tactic:
rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]

Premises used: Nat.mul_succ, mul_left_comm, Finset.prod_range_succ_comm, integral_sin_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
succ :
  (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / (↑(2 * k + 1 + 2) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(2 * k + 1 + 1) : ℝ) (↑(2 * k + 1 + 2) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    HDiv.hDiv (α := ℝ) (↑(2 * k + 2) : ℝ) (↑(2 * k + 3) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * k + 1) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * k + 1) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * k + 1) : ℝ) 2 *
        ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 3) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
succ :
  sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π +
      HMul.hMul (α := ℝ) (↑(2 * k + 1 + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) =
    HMul.hMul (α := ℝ) (↑(2 * k + 1 + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1))
⊢ (sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π) / (↑(2 * k + 1 + 2) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(2 * k + 1 + 1) : ℝ) (↑(2 * k + 1 + 2) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    HDiv.hDiv (α := ℝ) (↑(2 * k + 2) : ℝ) (↑(2 * k + 3) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
⊢ sin 0 ^ (2 * k + 1 + 1) * cos 0 - sin π ^ (2 * k + 1 + 1) * cos π +
      HMul.hMul (α := ℝ) (↑(2 * k + 1 + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)) =
    HMul.hMul (α := ℝ) (↑(2 * k + 1 + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
zero :
  ∫ (x : ℝ) in 0..π, sin x ^ (HMul.hMul (α := ℕ) 2 0 + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range 0, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
succ :
  ∀ (k : ℕ)
    (ih :
      ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) =
        HMul.hMul (α := ℝ) 2
          (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))),
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1) + 1) =
      HMul.hMul (α := ℝ) 2
        (∏ i ∈ Finset.range (k + 1), (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 1) =
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))

Tactic:
induction n with
  | zero => norm_num
  | succ k ih =>
    rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
    norm_cast
    field_simp
    simp

Premises used: Nat.mul_succ, mul_left_comm, Finset.prod_range_succ_comm, Nat.zero, integral_sin_pow, Nat.succ
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ HMul.hMul (α := ℕ) 2 0 =
    π * ∏ i ∈ Finset.range 0, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
succ :
  (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) =
    π * ∏ i ∈ Finset.range (k + 1), (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)

Tactic:
rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]

Premises used: Nat.mul_succ, mul_left_comm, Finset.prod_range_succ_comm, integral_sin_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
succ :
  (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k + 2) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) (↑(2 * k + 2) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) (↑(2 * k + 2) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * k) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
succ :
  sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π +
      HMul.hMul (α := ℝ) (↑(2 * k + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k)) =
    HMul.hMul (α := ℝ) (↑(2 * k + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k + 2) : ℝ) +
      HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) (↑(2 * k + 2) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    HDiv.hDiv (α := ℝ) (↑(2 * k + 1) : ℝ) (↑(2 * k + 2) : ℝ) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n k : ℕ
ih :
  ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
    π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
⊢ sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π +
      HMul.hMul (α := ℝ) (↑(2 * k + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k)) =
    HMul.hMul (α := ℝ) (↑(2 * k + 1) : ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
zero :
  ∫ (x : ℝ) in 0..π, sin x ^ HMul.hMul (α := ℕ) 2 0 =
    π * ∏ i ∈ Finset.range 0, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
succ :
  ∀ (k : ℕ)
    (ih :
      ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) =
        π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)),
    ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) =
      π * ∏ i ∈ Finset.range (k + 1), (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * n) =
    π * ∏ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)

Tactic:
induction n with
  | zero => simp
  | succ k ih =>
    rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
    norm_cast
    field_simp
    simp

Premises used: Nat.mul_succ, mul_left_comm, Finset.prod_range_succ_comm, Nat.zero, integral_sin_pow, Nat.succ
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
inl : ∀ (k : ℕ), LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
inr : ∀ (k : ℕ), LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1))
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ n)

Tactic:
rcases even_or_odd' n with ⟨k, rfl | rfl⟩

Premises used: Nat.even_or_odd', rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k : ℕ
inl : 0 < π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))

Tactic:
simp only [integral_sin_pow_even, integral_sin_pow_odd]

Premises used: integral_sin_pow_odd, integral_sin_pow_even
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k : ℕ
inr :
  0 <
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1))

Tactic:
simp only [integral_sin_pow_even, integral_sin_pow_odd]

Premises used: integral_sin_pow_odd, integral_sin_pow_even
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k : ℕ
⊢ 0 < π

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k : ℕ
inl : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1
inl₁ : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2
⊢ 0 < π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)

Tactic:
refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_)

Premises used: mul_pos, Finset.prod_pos, Nat.div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k : ℕ
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k : ℕ
inr : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2
inr₁ : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3
⊢ 0 <
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))

Tactic:
refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_)

Premises used: mul_pos, Finset.prod_pos, Nat.div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k n : ℕ
h : n ∈ Finset.range k
inl : 0 < 2 * n + 1
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k n : ℕ
h : n ∈ Finset.range k
inl : 0 < 2 * n + 2
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k n : ℕ
h : n ∈ Finset.range k
inr : 0 < 2 * n + 2
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k n : ℕ
h : n ∈ Finset.range k
inr : 0 < 2 * n + 3
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k n : ℕ
h : n ∈ Finset.range k
⊢ 0 < 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k n : ℕ
h : n ∈ Finset.range k
⊢ 0 < 2 * n + 2

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
k n : ℕ
h : n ∈ Finset.range k
⊢ 0 < 2 * n + 3

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
H : ∀ (x : ℝ) (h : x ∈ Set.Icc 0 π), sin x ^ (n + 1) ≤ sin x ^ n := ⋯
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (n + 1)) (∫ (x : ℝ) in 0..π, sin x ^ n)

Tactic:
integral_mono_on pi_pos.le ?_ ?_ H

Premises used: intervalIntegral.integral_mono_on, Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
H : ∀ (x : ℝ) (h : x ∈ Set.Icc 0 π), sin x ^ (n + 1) ≤ sin x ^ n := ⋯
refine_1 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ (n + 1)) MeasureTheory.volume 0 π
refine_2 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume 0 π
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (n + 1)) (∫ (x : ℝ) in 0..π, sin x ^ n)

Tactic:
refine integral_mono_on pi_pos.le ?_ ?_ H

Premises used: intervalIntegral.integral_mono_on, Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
H : ∀ (x : ℝ) (h : x ∈ Set.Icc 0 π), sin x ^ (n + 1) ≤ sin x ^ n := ⋯
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ (n + 1)) MeasureTheory.volume 0 π

Tactic:
(continuous_sin.pow _).intervalIntegrable 0 π

Premises used: Real.pi, Continuous.pow, Real.continuous_sin, Continuous.intervalIntegrable, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
H : ∀ (x : ℝ) (h : x ∈ Set.Icc 0 π), sin x ^ (n + 1) ≤ sin x ^ n := ⋯
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ (n + 1)) MeasureTheory.volume 0 π

Tactic:
exact (continuous_sin.pow _).intervalIntegrable 0 π

Premises used: Real.pi, Continuous.pow, Real.continuous_sin, Continuous.intervalIntegrable, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
H : ∀ (x : ℝ) (h : x ∈ Set.Icc 0 π), sin x ^ (n + 1) ≤ sin x ^ n := ⋯
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume 0 π

Tactic:
(continuous_sin.pow _).intervalIntegrable 0 π

Premises used: Real.pi, Continuous.pow, Real.continuous_sin, Continuous.intervalIntegrable, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
n : ℕ
H : ∀ (x : ℝ) (h : x ∈ Set.Icc 0 π), sin x ^ (n + 1) ≤ sin x ^ n := ⋯
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume 0 π

Tactic:
exact (continuous_sin.pow _).intervalIntegrable 0 π

Premises used: Real.pi, Continuous.pow, Real.continuous_sin, Continuous.intervalIntegrable, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
⊢ Antitone (β := ℝ) fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
antitone_nat_of_succ_le integral_sin_pow_succ_le

Premises used: antitone_nat_of_succ_le, integral_sin_pow_succ_le
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
α β γ : ℝ
⊢ β * α * γ * α = β * (α * α * γ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
⊢ ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)

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