awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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] (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))
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] (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
-- 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] (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))
have 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
Tactic: linear_combination (norm := (push_cast; ring_nf)) h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (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))
have 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))
Tactic: have h := one_sub_X_sq_mul_iterate_derivative_T_eval (R := R) n k 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
⊢ (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))
have 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))
Tactic: rw [one_pow, sub_self, zero_mul, mul_one] 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 : ℕ
⊢ (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))
have 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))
Tactic: have h := one_sub_X_sq_mul_iterate_derivative_U_eval (R := R) n k 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
⊢ (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))
have 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))
Tactic: rw [one_pow, sub_self, zero_mul, mul_one] 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 : ℕ
⊢ 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))
have 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))
Tactic: have h := one_sub_X_sq_mul_iterate_derivative_T_eval (R := R) n k 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
have 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)))
Tactic: rw [zero_pow two_ne_zero, sub_zero, one_mul, mul_zero, zero_mul, zero_sub] 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 :
  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))
have 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
Tactic: linear_combination (norm := (push_cast; ring_nf)) h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ 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))
have 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))
Tactic: have h := one_sub_X_sq_mul_iterate_derivative_U_eval (R := R) n k 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
have 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)))
Tactic: rw [zero_pow two_ne_zero, sub_zero, one_mul, mul_zero, zero_mul, zero_sub] 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 :
  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))
have 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
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 : ℕ
⊢ (↑(∏ 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)
have 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)
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ (↑(∏ 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)
have 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)
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ (↑(∏ 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)
have 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)
Tactic: push_cast at ih ⊢
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
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)
have rw : (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
    eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
  ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 1),
      mul_assoc, iterate_derivative_T_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
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)
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (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)
have rw₁ : ((HMul.hMul (α := R) 2 (↑k : R) + 1) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
    eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
  ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 1),
      mul_assoc, iterate_derivative_T_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
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)
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
rw₁ :
  ((HMul.hMul (α := R) 2 (↑k : R) + 1) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (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)
have rw₂ : (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) * (HMul.hMul (α := R) 2 (↑k : R) + 1) *
    eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
  ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 1),
      mul_assoc, iterate_derivative_T_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
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)
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
rw₁ :
  ((HMul.hMul (α := R) 2 (↑k : R) + 1) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
rw₂ :
  (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) * (HMul.hMul (α := R) 2 (↑k : R) + 1) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (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)
have rw₃ : (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
    ((HMul.hMul (α := R) 2 (↑k : R) + 1) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n))) =
  ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 1),
      mul_assoc, iterate_derivative_T_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
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)
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
rw₁ :
  ((HMul.hMul (α := R) 2 (↑k : R) + 1) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
rw₂ :
  (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) * (HMul.hMul (α := R) 2 (↑k : R) + 1) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) =
    ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
rw₃ :
  (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
      ((HMul.hMul (α := R) 2 (↑k : R) + 1) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n))) =
    ∏ x ∈ insert k (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)
have rw₄ : (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
    ((HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) =
  ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 1),
      mul_assoc, iterate_derivative_T_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self]