-- 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) + 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)
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)
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)
rw₈ :
  (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      ∏ x ∈ Finset.range k, (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2) =
    ∏ x ∈ insert k (Finset.range k), (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2)
rw₉ rw₁₀ :
  (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      ∏ x ∈ Finset.range k, (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑x : R) 2) =
    (HPow.hPow (α := R) (β := ℕ) (↑n : R) 2 - HPow.hPow (α := R) (β := ℕ) (↑k : R) 2) *
      ∏ 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:
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]

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