-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
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
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
rw₆ :
  ((HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        ∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
      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
rw₇ :
  (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      ((∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
        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
rw₈ :
  (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      ((∏ 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 ∈ 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₉ :
  (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      ((∏ 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) =
    ((HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
        ∏ 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₁₀ rw₁₁ :
  (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      ((∏ 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) =
    (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑k : R) 1) 2) *
      ((∏ 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:
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]

Premises used: Finset.prod_insert, HMul.hMul, mul_assoc, HSub.hSub, Finset.range_add_one, Polynomial.Chebyshev.iterate_derivative_U_eval_one_recurrence, HPow.hPow, HAdd.hAdd, Finset.notMem_range_self, mul_comm, OfNat.ofNat