awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
Tactic: have hv₂ (x) : HasDerivAt v₂ (v₂' x) x := (hasDerivAt_mul_const θ).cos
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have h : (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
  (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ
Tactic: convert_to (∫ (x : ℝ) in (-1)..1, u₁ x * v₁' x) * θ = _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
h :
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have convert_2 : (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ =
  -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
    4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
Tactic: convert_to (∫ (x : ℝ) in (-1)..1, u₁ x * v₁' x) * θ = _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
h :
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, f x ^ (n + 1) * v₁' x) * θ
h₁ :
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, f x ^ (n + 1) * (cos (x * θ) * θ)) * θ
h₂ :
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * (cos (x * θ) * θ)) * θ
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ
have h₃ : Eq (α := ℝ) (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ) * HPow.hPow (β := ℕ) θ 2)
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * (cos (x * θ) * θ) * θ)
Tactic: simp_rw [u₁, v₁', f, ← intervalIntegral.integral_mul_const, sq θ, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
h :
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, f x ^ (n + 1) * v₁' x) * θ
h₁ :
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, f x ^ (n + 1) * (cos (x * θ) * θ)) * θ
h₂ :
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * (cos (x * θ) * θ)) * θ
h₃ :
  Eq (α := ℝ) (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ) * HPow.hPow (β := ℕ) θ 2)
    (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * (cos (x * θ) * θ) * θ)
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ
have h₄ : Eq (α := ℝ) (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ) * (θ * θ))
  (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * (cos (x * θ) * θ) * θ)
Tactic: simp_rw [u₁, v₁', f, ← intervalIntegral.integral_mul_const, sq θ, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ (∫ (x : ℝ) in -1..1, u₁ x * v₁' x) * θ =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have convert_2 : ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ =
  -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
    4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
Tactic: rw [integral_mul_deriv_eq_deriv_mul (fun x _ => hu₁ x) (fun x _ => hv₁ x)
    (hu₁d.intervalIntegrable _ _) (hv₁d.intervalIntegrable _ _), hu₁_eval_one, hu₁_eval_neg_one,
    zero_mul, zero_mul, sub_zero, zero_sub, ← integral_neg, ← integral_mul_const]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have h : ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x
Tactic: convert_to ((-2 : ℝ) * (n + 1)) * ∫ (x : ℝ) in (-1)..1, (u₂ x * v₂' x) = _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
h : ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have convert_2 : -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x =
  -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
    4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
Tactic: convert_to ((-2 : ℝ) * (n + 1)) * ∫ (x : ℝ) in (-1)..1, (u₂ x * v₂' x) = _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x
have h : Eq (α := ℝ) (∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ)
  (∫ (x : ℝ) in -1..1, -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (u₂ x * v₂' x))
Tactic: rw [← integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ)
    (∫ (x : ℝ) in -1..1, -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (u₂ x * v₂' x))
have h : ∀ (x : ℝ), -(u₁' x * v₁ x) * θ = -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (u₂ x * v₂' x)
Tactic: congr 1 with x
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have convert_2 : -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (2 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, u₂' x * v₂ x =
  -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
    4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
Tactic: rw [integral_mul_deriv_eq_deriv_mul (fun x _ => hu₂ x) (fun x _ => hv₂ x)
    (hu₂d.intervalIntegrable _ _) (hv₂d.intervalIntegrable _ _),
    mul_sub, t, neg_mul, neg_mul, neg_mul, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
⊢ u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
have zero : let u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ HAdd.hAdd (α := ℕ) 0 1;
let u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * x * HPow.hPow (β := ℕ) (f x) 0);
let u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * HPow.hPow (β := ℕ) (f x) 0;
let u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦
  HPow.hPow (β := ℕ) (f x) 0 - HMul.hMul (α := ℝ) 2 (↑0 : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ HSub.hSub (α := ℕ) 0 1;
∀ (hu₁d : Continuous u₁') (hu₂d : Continuous u₂') (hu₁_eval_one : u₁ 1 = 0) (hu₁_eval_neg_one : u₁ (-1) = 0)
  (t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) (β := ℕ) 0 0 * cos θ))
  (hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x) (hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x),
  u₂' x =
    (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1) * HPow.hPow (β := ℕ) (f x) 0 -
      HMul.hMul (α := ℝ) 2 (↑0 : ℝ) * f x ^ HSub.hSub (α := ℕ) 0 1
Tactic: cases n with
    | zero => simp [u₂']
    | succ n => ring!
Cleared hypotheses: n, u₁, u₁', u₂, u₂', hu₁d, hu₂d, hu₁_eval_one, hu₁_eval_neg_one, t, hu₁, hu₂