-- 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
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
⊢ (∏ 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]