awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) =
    HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
        HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
      HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) +
        (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
            HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
          HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) -
      ((HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
          (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
            (⇑derivative : (a : R[X]) → R[X])^[k] (T R n) +
        ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
          ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
            HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))))) =
    0
have a : (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) +
      (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
          HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
        HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * (⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
    ((HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
        (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
          (⇑derivative : (a : R[X]) → R[X])^[k] (T R n) +
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
        ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
          HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))))) =
  0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) =
    HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
        HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
      HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) +
        (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
            HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
          HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * (⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
      ((HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
          (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
            (⇑derivative : (a : R[X]) → R[X])^[k] (T R n) +
        ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
          ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
            HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))))) =
    0
have a : HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) (↑k : R[X]) +
      HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) (↑k : R[X]) * (↑(k - 1) : R[X]) -
    (⇑derivative : (a : R[X]) → R[X])^[k] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2 =
  0
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) =
    HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
        HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
      HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
      (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (T R n)
have a : HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) (↑k : R[X]) +
      HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) (↑k : R[X]) * (↑(k - 1) : R[X]) -
    (⇑derivative : (a : R[X]) → R[X])^[k] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2 =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf)) h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) =
    HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
        HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
      HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) (↑k : R[X]) +
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) (↑k : R[X]) * (↑(k - 1) : R[X]) -
      (⇑derivative : (a : R[X]) → R[X])^[k] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2 =
    0
have a : ∀
  (h :
    (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] (T R n) -
        ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HSMul.hSMul (β := R[X]) (HMul.hMul (α := ℕ) 2 0)
                ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] (T R n)) *
              X +
          HSMul.hSMul (β := R[X]) (0 * HSub.hSub (α := ℕ) 0 1) ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n))) =
      HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] (T R n)) X +
          HSMul.hSMul (α := ℕ) (β := R[X]) 0 ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n)) -
        HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n))),
  HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n)) (↑0 : R[X]) +
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n)) (↑0 : R[X]) *
          (↑(HSub.hSub (α := ℕ) 0 1) : R[X]) -
      (⇑derivative : (a : R[X]) → R[X])^[0] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑0 : R[X]) 2 =
    0
Tactic: cases k
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 3) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 -
          HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (U R n)
have h : (⇑derivative : (a : R[X]) → R[X])^[k]
    ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (U R n)) =
  (⇑derivative : (a : R[X]) → R[X])^[k]
    (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n)
Tactic: have h := congr_arg derivative^[k] <| one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U
    (R := R) n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (U R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n)
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 3) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 -
          HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (U R n)
have h₁ : (⇑derivative : (a : R[X]) → R[X])^[k]
    ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (U R n)) =
  (⇑derivative : (a : R[X]) → R[X])^[k]
    (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) (U R n))
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (U R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
        HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) (U R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 3) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 -
          HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (U R n)
have h₁ : (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
    ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
      HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) =
  (↑3 : R[X]) *
      (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
        HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
    HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
Tactic: rw [sub_mul, iterate_derivative_sub, one_mul, ← Function.iterate_add_apply, mul_comm (X ^ 2),
    iterate_derivative_sub, mul_assoc 3, ← Nat.cast_three, iterate_derivative_natCast_mul,
    mul_comm X, iterate_derivative_intCast_mul, iterate_derivative_derivative_mul_X_sq,
    iterate_derivative_derivative_mul_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) =
    (↑3 : R[X]) *
        (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
          HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) +
        ((↑3 : R[X]) *
            (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
              HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
          HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      ((HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 3) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n) -
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1) 2) *
            (⇑derivative : (a : R[X]) → R[X])^[k] (U R n) +
        ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
          ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
            HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))))) =
    0
have a : (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) +
      (3 *
          (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
            HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) -
    ((HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 3) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n) -
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 -
            HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1) 2) *
          (⇑derivative : (a : R[X]) → R[X])^[k] (U R n) +
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
        ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
          HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))))) =
  0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) =
    (↑3 : R[X]) *
        (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
          HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) +
        (3 *
            (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
              HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) -
      ((HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 3) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n) -
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1) 2) *
            (⇑derivative : (a : R[X]) → R[X])^[k] (U R n) +
        ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
          ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
              HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
            HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))))) =
    0
have a : HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) (↑k : R[X]) +
      HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) (↑k : R[X]) * (↑(k - 1) : R[X]) -
    (⇑derivative : (a : R[X]) → R[X])^[k] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2 =
  0
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) =
    (↑3 : R[X]) *
        (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
          HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 3) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) 2 -
          HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (↑k : R[X]) 1) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (U R n)
have a : HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) (↑k : R[X]) +
      HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) (↑k : R[X]) * (↑(k - 1) : R[X]) -
    (⇑derivative : (a : R[X]) → R[X])^[k] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2 =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf)) h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) =
    (↑3 : R[X]) *
        (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) X +
          HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) (↑k : R[X]) +
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) (↑k : R[X]) * (↑(k - 1) : R[X]) -
      (⇑derivative : (a : R[X]) → R[X])^[k] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2 =
    0
have a : ∀
  (h :
    (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] (U R n) -
        ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
            HSMul.hSMul (β := R[X]) (HMul.hMul (α := ℕ) 2 0)
                ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] (U R n)) *
              X +
          HSMul.hSMul (β := R[X]) (0 * HSub.hSub (α := ℕ) 0 1) ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n))) =
      (↑3 : R[X]) *
          (HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] (U R n)) X +
            HSMul.hSMul (α := ℕ) (β := R[X]) 0 ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n))) -
        HMul.hMul (α := R[X]) (↑((n + 2) * n) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n))),
  HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n)) (↑0 : R[X]) +
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n)) (↑0 : R[X]) *
          (↑(HSub.hSub (α := ℕ) 0 1) : R[X]) -
      (⇑derivative : (a : R[X]) → R[X])^[0] (U R n) * HPow.hPow (α := R[X]) (β := ℕ) (↑0 : R[X]) 2 =
    0
Tactic: cases k
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
x : R
⊢ (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
have h : Eq.{u_1 + 1} (α := R)
  ((fun (p : R[X]) ↦ eval x p)
    ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)))
  ((fun (p : R[X]) ↦ eval x p)
    ((HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
      (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (T R n)))
Tactic: have h := congr_arg (fun (p : R[X]) => p.eval x) <|
    one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T n k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
x : R
h :
  (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
have a : (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) +
      ((HMul.hMul (α := R) 2 (↑k : R) + 1) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
        (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
          eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) -
    ((HMul.hMul (α := R) 2 (↑k : R) + 1) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
        (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
          eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) +
      (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n))) =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf)) h