awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
x : ℝ
⊢ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1) =
    1 * f x ^ n + x * ((↑n : ℝ) * f x ^ (n - 1) * (-2 * x))

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
⊢ ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x

Tactic:
have hu₂ (x) : HasDerivAt u₂ (u₂' x) x := by
    convert! (hasDerivAt_id' x).fun_mul ((hf x).fun_pow _) using 1
    simp only [u₂']
    ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 : ℝ), HasDerivAt v₂ (v₂' x) x

Tactic:
have hv₂ (x) : HasDerivAt v₂ (v₂' x) x := (hasDerivAt_mul_const θ).cos
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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) * θ
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) θ
⊢ (∫ (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) θ

Tactic:
convert_to (∫ (x : ℝ) in (-1)..1, u₁ x * v₁' x) * θ = _ using 1

Premises used: HMul.hMul, intervalIntegral, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 * θ) * θ) * θ)
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 * θ) * θ) * θ)
⊢ (∫ (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:
simp_rw [u₁, v₁', f, ← intervalIntegral.integral_mul_const, sq θ, mul_assoc]

Premises used: mul_assoc, sq, intervalIntegral.integral_mul_const
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
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) θ
⊢ (∫ (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]

Premises used: sub_zero, MulZeroClass.zero_mul, intervalIntegral.integral_mul_deriv_eq_deriv_mul, Continuous.intervalIntegrable, intervalIntegral.integral_neg, intervalIntegral.integral_mul_const, zero_sub
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
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) θ
⊢ ∫ (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

Premises used: HMul.hMul, Nat.cast, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 :
  Eq (α := ℝ) (∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ)
    (∫ (x : ℝ) in -1..1, -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (u₂ x * v₂' x))
⊢ ∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ = -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, u₂ x * v₂' x

Tactic:
rw [← integral_const_mul]

Premises used: intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 : ℝ), -(u₁' x * v₁ x) * θ = -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (u₂ x * v₂' x)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -1..1, -(u₁' x * v₁ x) * θ)
    (∫ (x : ℝ) in -1..1, -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (u₂ x * v₂' x))

Tactic:
congr 1 with x
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 : ℝ
h :
  -(-(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n) * sin (x * θ)) * θ =
    -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x * f x ^ n * (-sin (x * θ) * θ))
⊢ -(u₁' x * v₁ x) * θ = -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (u₂ x * v₂' x)

Tactic:
dsimp [u₁', v₁, u₂, v₂']
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 : ℝ
⊢ -(-(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n) * sin (x * θ)) * θ =
    -2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x * f x ^ n * (-sin (x * θ) * θ))

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
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) θ
⊢ -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]

Premises used: mul_sub, intervalIntegral.integral_mul_deriv_eq_deriv_mul, Continuous.intervalIntegrable, neg_mul, sub_neg_eq_add
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hv₁d : Continuous v₁'
hv₂d : Continuous v₂'
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ HAdd.hAdd (α := ℕ) 0 1
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * x * HPow.hPow (β := ℕ) (f x) 0)
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * HPow.hPow (β := ℕ) (f x) 0
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:
simp [u₂']
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hv₁d : Continuous v₁'
hv₂d : Continuous v₂'
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
n : ℕ
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1 + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * x * f x ^ (n + 1))
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ (n + 1)
u₂' : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦ f x ^ (n + 1) - HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n + 1 - 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 (n + 1) * cos θ)
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
⊢ u₂' x =
    (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) * f x ^ (n + 1) - HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) * f x ^ (n + 1 - 1)

Tactic:
ring!