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
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
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
succ :
  ∀ (n : ℕ),
    let u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1 + 1);
    let u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * x * f x ^ (n + 1));
    let u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ (n + 1);
    let 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)
⊢ u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)

Tactic:
cases n with
    | zero => simp [u₂']
    | succ n => 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
⊢ ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)

Tactic:
have (x : _) : u₂' x = (2 * n + 1) * f x ^ n - 2 * n * f x ^ (n - 1) := by
    cases n with
    | zero => simp [u₂']
    | succ n => 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
this : ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
convert_2 :
  -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (2 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
        ∫ (x : ℝ) in -1..1,
          (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x) -
            HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * 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 * (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:
simp_rw [this, sub_mul, mul_assoc _ _ (v₂ _)]

Premises used: mul_assoc, sub_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
this : ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
⊢ Continuous v₂

Tactic:
fun_prop
-- 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
this : ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
⊢ Continuous v₂

Tactic:
have : Continuous v₂ := by fun_prop
-- 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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
convert_2 :
  -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      ((2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
          ∫ (x : ℝ) in -1..1, (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)) -
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
          ∫ (x : ℝ) in -1..1, HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * 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) θ)
convert_2₁ :
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)) volume (-1) 1
convert_2₂ :
  IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * v₂ x)) volume (-1) 1
⊢ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (2 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
        ∫ (x : ℝ) in -1..1,
          (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x) -
            HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * 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 [mul_mul_mul_comm, integral_sub, mul_sub, add_sub_assoc]

Premises used: add_sub_assoc, mul_mul_mul_comm, mul_sub, intervalIntegral.integral_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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
convert_2 :
  (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)) -
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * v₂ x) =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
⊢ -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
      ((2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
          ∫ (x : ℝ) in -1..1, (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)) -
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
          ∫ (x : ℝ) in -1..1, HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * 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:
congr 1
-- 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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
convert_2 :
  2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * ∫ (x : ℝ) in -1..1, f x ^ n * v₂ x) -
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) * ∫ (x : ℝ) in -1..1, f x ^ (n - 1) * v₂ x) =
    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, (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)) -
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ∫ (x : ℝ) in -1..1, HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * v₂ x) =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ

Tactic:
simp_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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
⊢ 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * ∫ (x : ℝ) in -1..1, f x ^ n * v₂ x) -
      2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) * ∫ (x : ℝ) in -1..1, f x ^ (n - 1) * v₂ x) =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ

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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)

Tactic:
fun_prop
-- 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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)) volume (-1) 1

Tactic:
exact Continuous.intervalIntegrable (by fun_prop) _ _

Premises used: Continuous.intervalIntegrable
-- 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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * v₂ x)

Tactic:
fun_prop
-- 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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * v₂ x)) volume (-1) 1

Tactic:
exact Continuous.intervalIntegrable (by fun_prop) _ _

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
rw :
  -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * (HPow.hPow (α := ℝ) 0 (n + 1) * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1) * I (n + 1) θ -
      4 * HAdd.hAdd (α := ℝ) (↑(n + 1) : ℝ) 1 * (↑(n + 1) : ℝ) * I (n + 1 - 1) θ =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * I (n + 1) θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ
⊢ I (n + 2) θ * HPow.hPow (β := ℕ) θ 2 =
    2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 3) * I (n + 1) θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ

Tactic:
rw [recursion' (n + 1)]

Premises used: _private.0.recursion', HAdd.hAdd, OfNat.ofNat