awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
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
⊢ u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
have 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)
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₂
-- 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
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
⊢ -(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) θ
have this : ∀ (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!
-- 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
this : ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (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) θ
have 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) θ
Tactic: simp_rw [this, sub_mul, mul_assoc _ _ (v₂ _)]
-- 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
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)
⊢ -(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) θ
have this₁ : Continuous v₂
Tactic: have : Continuous v₂ := by fun_prop
-- 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
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 * (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) θ
have 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) θ)
Tactic: rw [mul_mul_mul_comm, integral_sub, mul_sub, add_sub_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
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) θ)
⊢ -(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) θ
have convert_2₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * (f x ^ n * v₂ x)) volume (-1) 1
Tactic: rw [mul_mul_mul_comm, integral_sub, mul_sub, add_sub_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
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
⊢ -(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) θ
have convert_2₂ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (f x ^ (n - 1) * v₂ x)) volume (-1) 1
Tactic: rw [mul_mul_mul_comm, integral_sub, mul_sub, add_sub_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
this_1 :
  ∀ (x : ℝ), u₂' x = (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * f x ^ (n - 1)
this : Continuous v₂
⊢ -(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) θ)
have 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) θ
Tactic: congr 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
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 * ∫ (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) θ
have 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) θ
Tactic: simp_rw [integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
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 θ
have 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 θ
Tactic: rw [recursion' (n + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
n : ℕ
⊢ -(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 θ
have push_cast : -(HMul.hMul (α := ℝ) 2 2 * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (HPow.hPow (α := ℝ) 0 (n + 1) * cos θ))) +
      2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * (2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * I (n + 1) θ -
    4 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + 1) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * I n θ =
  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: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
⊢ I 1 θ * HPow.hPow (β := ℕ) θ 3 = 4 * sin θ - 4 * θ * cos θ
have rw : -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (HPow.hPow (α := ℝ) (β := ℕ) 0 0 * cos θ))) * θ +
      2 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑0 : ℝ) + 1) * (2 * sin θ) -
    4 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 * (↑0 : ℝ) * I (HSub.hSub (α := ℕ) 0 1) θ * θ =
  4 * sin θ - 4 * θ * cos θ
Tactic: rw [_root_.pow_succ, ← mul_assoc, recursion' 0, sub_mul, add_mul, mul_assoc _ (I 0 θ), I_zero]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • sinPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤
    n + 2
have refine_1 : (sinPoly (n + 1)).natDegree ≤ n + 2
Tactic: refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
refine_1 : (sinPoly (n + 1)).natDegree ≤ n + 2
⊢ ((2 * (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 3)) • sinPoly (n + 1) +
        (monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤
    n + 2
have refine_2 : ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤ n + 2
Tactic: refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
n : ℕ
⊢ ((monomial 2 : (a : ℤ) → ℤ[X]) (-4) * sinPoly n).natDegree ≤ n + 2
have refine_2 : natDegree (R := ℤ) ((monomial 2 : (a : ℤ) → ℤ[X]) (-4)) + (sinPoly n).natDegree ≤ n + 2
Tactic: refine natDegree_mul_le.trans ?_