awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
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
⊢ (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))

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
x : R
⊢ 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] (U R n)))
    ((fun (p : R[X]) ↦ eval x p)
      ((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)))

Tactic:
have h := congr_arg (fun (p : R[X]) => p.eval x) <|
    one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U n k
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
x : R
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] (U R n)))
    ((fun (p : R[X]) ↦ eval x p)
      ((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)))
⊢ (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
simp only [eval_mul, eval_sub, eval_one, eval_pow,
    eval_X, eval_add, eval_ofNat, eval_natCast, eval_intCast] at h

Premises used: Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_natCast, Polynomial.eval_mul, Polynomial.eval_intCast, Polynomial.eval_add, Polynomial.eval_one, Polynomial.eval_ofNat, Polynomial.eval_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) +
        ((HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
            eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      ((HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
            eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) +
        (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
a :
  (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) +
        ((HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
            eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      ((HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
            eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) +
        (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n))) =
    0
⊢ (1 - HPow.hPow (β := ℕ) x 2) * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * x * eval x ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval x ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (1 - HPow.hPow (α := R) (β := ℕ) 1 2) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * 1 * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_T_eval (R := R) n k 1
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (1 - HPow.hPow (α := R) (β := ℕ) 1 2) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * 1 * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ 0 =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))

Tactic:
rw [one_pow, sub_self, zero_mul, mul_one] at h

Premises used: one_pow, sub_self, MulZeroClass.zero_mul, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  0 =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ (HMul.hMul (α := R) 2 (↑k : R) + 1) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))

Tactic:
sub_eq_zero.mp h.symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  0 =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ (HMul.hMul (α := R) 2 (↑k : R) + 1) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))

Tactic:
exact sub_eq_zero.mp h.symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (1 - HPow.hPow (α := R) (β := ℕ) 1 2) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * 1 * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_U_eval (R := R) n k 1
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (1 - HPow.hPow (α := R) (β := ℕ) 1 2) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * 1 * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ 0 =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
rw [one_pow, sub_self, zero_mul, mul_one] at h

Premises used: one_pow, sub_self, MulZeroClass.zero_mul, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  0 =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ (HMul.hMul (α := R) 2 (↑k : R) + 3) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
sub_eq_zero.mp h.symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  0 =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ (HMul.hMul (α := R) 2 (↑k : R) + 3) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
exact sub_eq_zero.mp h.symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (1 - HPow.hPow (α := R) (β := ℕ) 0 2) * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * 0 * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_T_eval (R := R) n k 0
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (1 - HPow.hPow (α := R) (β := ℕ) 0 2) * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 1) * 0 * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) -
      (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    -((HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)))

Tactic:
rw [zero_pow two_ne_zero, sub_zero, one_mul, mul_zero, zero_mul, zero_sub] at h

Premises used: sub_zero, MulZeroClass.zero_mul, MulZeroClass.mul_zero, two_ne_zero, zero_pow, one_mul, zero_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    -((HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)))
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) +
        -((HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
            eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) -
      (-(HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
          eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) +
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    -((HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)))
a :
  eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) +
        -((HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
            eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) -
      (-(HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
          eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) +
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n))) =
    0
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n)) =
    -(HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (1 - HPow.hPow (α := R) (β := ℕ) 0 2) * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * 0 * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
have h := one_sub_X_sq_mul_iterate_derivative_U_eval (R := R) n k 0
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (1 - HPow.hPow (α := R) (β := ℕ) 0 2) * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    (HMul.hMul (α := R) 2 (↑k : R) + 3) * 0 * eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) -
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    -((HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)))

Tactic:
rw [zero_pow two_ne_zero, sub_zero, one_mul, mul_zero, zero_mul, zero_sub] at h

Premises used: sub_zero, MulZeroClass.zero_mul, MulZeroClass.mul_zero, two_ne_zero, zero_pow, one_mul, zero_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    -((HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)))
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) +
        -((HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
            eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      (-(HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
          eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) +
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    -((HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)))
a :
  eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) +
        -((HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
            eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))) -
      (-(HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
          eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) +
        eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n))) =
    0
⊢ eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (U R n)) =
    -(HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      eval 0 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n))

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
induction :
  (↑(∏ l ∈ Finset.range 0, (2 * l + 1)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n)) =
    (↑(∏ l ∈ Finset.range 0, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R)
succ :
  ∀ (n_1 : ℕ),
    (↑(∏ l ∈ Finset.range n_1, (2 * l + 1)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[n_1] (T R n)) =
        (↑(∏ l ∈ Finset.range n_1, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R) →
      (↑(∏ l ∈ Finset.range (n_1 + 1), (2 * l + 1)) : R) *
          eval 1 ((⇑derivative : (a : R[X]) → R[X])^[n_1 + 1] (T R n)) =
        (↑(∏ l ∈ Finset.range (n_1 + 1), (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R)
⊢ (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R)

Tactic:
induction k
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (↑(∏ l ∈ Finset.range 0, (2 * l + 1)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n)) =
    (↑(∏ l ∈ Finset.range 0, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (↑(∏ l ∈ Finset.range 0, (2 * l + 1)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[0] (T R n)) =
    (↑(∏ l ∈ Finset.range 0, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R)

Tactic:
case zero => simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
ih :
  (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R)
push_cast :
  ∀
    (ih :
      (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
          eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) =
        ∏ x ∈ Finset.range k, (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)),
    (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
      ∏ x ∈ Finset.range (k + 1), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
⊢ (↑(∏ l ∈ Finset.range (k + 1), (2 * l + 1)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    (↑(∏ l ∈ Finset.range (k + 1), (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : R)

Tactic:
push_cast at ih ⊢
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
induction :
  (↑(∏ l ∈ Finset.range 0, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n)) =
    (↑(∏ l ∈ Finset.range 0, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1
succ :
  ∀ (n_1 : ℕ),
    (↑(∏ l ∈ Finset.range n_1, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[n_1] (U R n)) =
        (↑(∏ l ∈ Finset.range n_1,
                (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
            R) *
          HAdd.hAdd (α := R) (↑n : R) 1 →
      (↑(∏ l ∈ Finset.range (n_1 + 1), (2 * l + 3)) : R) *
          eval 1 ((⇑derivative : (a : R[X]) → R[X])^[n_1 + 1] (U R n)) =
        (↑(∏ l ∈ Finset.range (n_1 + 1),
                (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
            R) *
          HAdd.hAdd (α := R) (↑n : R) 1
⊢ (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
induction k
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (↑(∏ l ∈ Finset.range 0, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n)) =
    (↑(∏ l ∈ Finset.range 0, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (↑(∏ l ∈ Finset.range 0, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[0] (U R n)) =
    (↑(∏ l ∈ Finset.range 0, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
case zero => simp