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 : ℕ
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)
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)
⊢ (∏ 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]
-- 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)
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)
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)
⊢ (∏ 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₆ : ((HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 1)) *
    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]
-- 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 + 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
have 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
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 + 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
⊢ (↑(∏ 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
have 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
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 + 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
⊢ (↑(∏ l ∈ Finset.range (k + 1), (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (↑(∏ l ∈ Finset.range (k + 1),
            (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1
have push_cast : ∀
  (ih :
    (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
      (∏ x ∈ Finset.range k,
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
            HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
        HAdd.hAdd (α := R) (↑n : R) 1),
  (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ Finset.range (k + 1),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
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) + 3)) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
    (∏ x ∈ Finset.range k,
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ Finset.range (k + 1),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
have rw : (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
    eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
  (∏ x ∈ insert k (Finset.range k),
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
    HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 3),
      mul_assoc, iterate_derivative_U_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self, mul_assoc]
-- 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) + 3)) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
    (∏ x ∈ Finset.range k,
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ Finset.range (k + 1),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
have rw₁ : ((HMul.hMul (α := R) 2 (↑k : R) + 3) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
    eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
  (∏ x ∈ insert k (Finset.range k),
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
    HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 3),
      mul_assoc, iterate_derivative_U_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self, mul_assoc]
-- 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) + 3)) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
    (∏ x ∈ Finset.range k,
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw₁ :
  ((HMul.hMul (α := R) 2 (↑k : R) + 3) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ Finset.range (k + 1),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
have rw₂ : (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) * (HMul.hMul (α := R) 2 (↑k : R) + 3) *
    eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
  (∏ x ∈ insert k (Finset.range k),
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
    HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 3),
      mul_assoc, iterate_derivative_U_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self, mul_assoc]
-- 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) + 3)) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
    (∏ x ∈ Finset.range k,
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw₁ :
  ((HMul.hMul (α := R) 2 (↑k : R) + 3) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw₂ :
  (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) * (HMul.hMul (α := R) 2 (↑k : R) + 3) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ Finset.range (k + 1),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
have rw₃ : (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
    ((HMul.hMul (α := R) 2 (↑k : R) + 3) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n))) =
  (∏ x ∈ insert k (Finset.range k),
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
    HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 3),
      mul_assoc, iterate_derivative_U_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self, mul_assoc]
-- 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) + 3)) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
    (∏ x ∈ Finset.range k,
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw :
  (∏ x ∈ insert k (Finset.range k), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw₁ :
  ((HMul.hMul (α := R) 2 (↑k : R) + 3) * ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw₂ :
  (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) * (HMul.hMul (α := R) 2 (↑k : R) + 3) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
rw₃ :
  (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      ((HMul.hMul (α := R) 2 (↑k : R) + 3) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n))) =
    (∏ x ∈ insert k (Finset.range k),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (∏ x ∈ Finset.range (k + 1),
        (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
      HAdd.hAdd (α := R) (↑n : R) 1
have rw₄ : (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
    ((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))) =
  (∏ x ∈ insert k (Finset.range k),
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
    HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [Finset.range_add_one, Finset.prod_insert Finset.notMem_range_self, mul_comm (2 * _ + 3),
      mul_assoc, iterate_derivative_U_eval_one_recurrence, ← mul_assoc, mul_comm _ (_ ^ 2 - _ ^ 2),
      mul_assoc, ih, Finset.prod_insert Finset.notMem_range_self, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ HMul.hMul (α := R) 3 (eval 1 ((derivative : (a : R[X]) → R[X]) (U R n))) =
    HAdd.hAdd (α := R) (↑n : R) 2 * HAdd.hAdd (α := R) (↑n : R) 1 * (↑n : R)
have h : (↑(∏ l ∈ Finset.range 1, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[1] (U R n)) =
  (↑(∏ l ∈ Finset.range 1, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) : R) *
    HAdd.hAdd (α := R) (↑n : R) 1
Tactic: have h := iterate_derivative_U_eval_one (R := R) n 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  (↑(∏ l ∈ Finset.range 1, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[1] (U R n)) =
    (↑(∏ l ∈ Finset.range 1, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ HMul.hMul (α := R) 3 (eval 1 ((derivative : (a : R[X]) → R[X]) (U R n))) =
    HAdd.hAdd (α := R) (↑n : R) 2 * HAdd.hAdd (α := R) (↑n : R) 1 * (↑n : R)
have h₁ : HMul.hMul (α := R) (↑(HMul.hMul (α := ℕ) 2 0 + 3) : R) (eval 1 ((derivative : (a : R[X]) → R[X]) (U R n))) =
  (↑(HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) 2) : R) *
    HAdd.hAdd (α := R) (↑n : R) 1
Tactic: simp only [Finset.range_one, Finset.prod_singleton, Function.iterate_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) =
    HDiv.hDiv (α := 𝔽) (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
      (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽)
have rw : eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽) =
  (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
Tactic: rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_T_eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
rw :
  eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) =
    HDiv.hDiv (α := 𝔽) (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
      (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽)
have rw₁ : (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽) * eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) =
  (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
Tactic: rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_T_eval_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
rw :
  eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
rw₁ :
  (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽) * eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) =
    HDiv.hDiv (α := 𝔽) (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
      (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽)
have rw₂ : Eq.{u_3 + 1} (α := 𝔽) (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
  (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
Tactic: rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_T_eval_one]