awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
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
have 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
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
n : ℕ
⊢ (∫ (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
have 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)
Tactic: convert! eq_sub_iff_add_eq.mp (integral_sin_pow_aux n) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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))
⊢ ∫ (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))
have 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)
Tactic: rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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 π) / 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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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 π) / (↑(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)
have 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))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
n : ℕ
⊢ ∫ (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))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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))
⊢ ∫ (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))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) =
    π * ∏ i ∈ Finset.range (k + 1), (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
have 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)
Tactic: rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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 π) / 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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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 π) / (↑(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)
have 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))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * n) =
    π * ∏ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
have zero : ∫ (x : ℝ) in 0..π, sin x ^ HMul.hMul (α := ℕ) 2 0 =
  π * ∏ i ∈ Finset.range 0, (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * n) =
    π * ∏ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
n : ℕ
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ n)
have inl : ∀ (k : ℕ), LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
Tactic: rcases even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
n : ℕ
inl : ∀ (k : ℕ), LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ n)
have inr : ∀ (k : ℕ), LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1))
Tactic: rcases even_or_odd' n with ⟨k, rfl | rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k : ℕ
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k))
have inl : 0 < π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
Tactic: simp only [integral_sin_pow_even, integral_sin_pow_odd]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k : ℕ
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1))
have inr : 0 <
  HMul.hMul (α := ℝ) 2 (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
Tactic: simp only [integral_sin_pow_even, integral_sin_pow_odd]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k : ℕ
⊢ 0 < π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
have inl : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1
Tactic: refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k : ℕ
inl : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1
⊢ 0 < π * ∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2)
have inl₁ : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2
Tactic: refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k : ℕ
⊢ 0 <
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
have inr : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2
Tactic: refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k : ℕ
inr : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2
⊢ 0 <
    HMul.hMul (α := ℝ) 2
      (∏ i ∈ Finset.range k, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 2) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 3))
have inr₁ : ∀ n ∈ Finset.range k, 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3
Tactic: refine mul_pos (by simp [pi_pos]) (prod_pos fun n _ => div_pos ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k n : ℕ
h : n ∈ Finset.range k
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1
have inl : 0 < 2 * n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k n : ℕ
h : n ∈ Finset.range k
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2
have inl : 0 < 2 * n + 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k n : ℕ
h : n ∈ Finset.range k
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2
have inr : 0 < 2 * n + 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
k n : ℕ
h : n ∈ Finset.range k
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3
have inr : 0 < 2 * n + 3
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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)
have refine_1 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ (n + 1)) MeasureTheory.volume 0 π
Tactic: refine integral_mono_on pi_pos.le ?_ ?_ H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
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 π
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..π, sin x ^ (n + 1)) (∫ (x : ℝ) in 0..π, sin x ^ n)
have refine_2 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ sin x ^ n) MeasureTheory.volume 0 π
Tactic: refine integral_mono_on pi_pos.le ?_ ?_ H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
⊢ ∫ (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 h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
Tactic: have h : ∀ α β γ : ℝ, β * α * γ * α = β * (α * α * γ) := fun α β γ => by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
Goal:
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
⊢ ∫ (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 hu : ∀ 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (hypothesis)
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 : ℝ) 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 hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
Tactic: have hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x := fun x _ => hasDerivAt_sin x
-- 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
⊢ ∫ (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 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)
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 : ℝ := 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)
⊢ ∫ (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 refine_1 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ -(↑(n + 1) : ℝ) * sin x * cos 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 : ℝ := 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
⊢ ∫ (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 refine_2 : IntervalIntegrable cos 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 : ℝ := 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, 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)
have hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos 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 : ℝ := 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
⊢ 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)
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos 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 : ℝ := 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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos x ^ n) MeasureTheory.volume a b
have hf : Continuous (Y := ℝ) fun (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
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
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ cos x ^ (n + 2)) MeasureTheory.volume a b
have hg : Continuous (Y := ℝ) fun (x : ℝ) ↦ cos x ^ (n + 2)
Tactic: apply Continuous.intervalIntegrable