-- Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre
Goal:
n : ℕ
_ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n)
_₁ :
  (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] ((X - HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) ^ n) =
    (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
      (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m))
_₂ :
  Eq (α := ℤ[X])
    ((⇑derivative : (a : ℤ[X]) → ℤ[X])^[n]
      (∑ m ∈ range (n + 1), n.choose m • HPow.hPow (α := ℤ[X]) (-1) m * HPow.hPow (α := ℤ[X]) X (n + m)))
    (∑ x ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X x)
_₃ :
  Eq (α := ℤ[X])
    (∑ x ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑((n + x)! / x !) : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) ((↑(n.choose x) : ℤ) * HPow.hPow (α := ℤ) (-1) x) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X x)
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑n ! : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) i * (↑(n.choose i) : ℤ) * (↑((n + i).choose n) : ℤ)) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X i)
_₄ :
  ∑ i ∈ range (n + 1),
      HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((↑n ! : ℤ[X]) : ℤ[X])
          ((C : (a : ℤ) → ℤ[X]) (HPow.hPow (α := ℤ) (-1) i * (↑(n.choose i) : ℤ) * (↑((n + i).choose n) : ℤ)) : ℤ[X]) *
        HPow.hPow (α := ℤ[X]) X i =
    (↑n ! : ℤ[X]) * shiftedLegendre n
⊢ (⇑derivative : (a : ℤ[X]) → ℤ[X])^[n] (HPow.hPow (α := ℤ[X]) X n * HSub.hSub (α := ℤ[X]) 1 X ^ n) =
    (↑n ! : ℤ[X]) * shiftedLegendre n

Tactic:
calc
  _ = derivative^[n] (((X : ℤ[X]) - X ^ 2) ^ n) := by
    rw [← mul_pow, mul_one_sub, ← pow_two]
  _ = derivative^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) := by
    congr
    rw [sub_eq_add_neg, add_comm, add_pow]
    congr! 1 with m hm
    rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc,
      ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm]
    rw [Finset.mem_range] at hm
    linarith
  _ = ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x := by
    rw [iterate_derivative_sum]
    congr! 1 with x _
    rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
    simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
    ring
  _ = ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i := by
    congr! 2 with x _
    rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]
    congr 1
    rw [add_comm, add_choose]
    simp only [Int.natCast_ediv, cast_mul, eq_intCast]
    norm_cast
    rw [mul_comm, ← Nat.mul_div_assoc]
    · rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
    · simp only [factorial_mul_factorial_dvd_factorial_add]
  _ = (n ! : ℤ[X]) * (shiftedLegendre n) := by simp [← mul_assoc, shiftedLegendre, mul_sum]

Premises used: Polynomial.derivative, Nat.choose, HMul.hMul, HSub.hSub, Nat.iterate, Nat.cast, Finset.range, HPow.hPow, HAdd.hAdd, Nat.factorial, HSMul.hSMul, OfNat.ofNat, Polynomial.X, DFunLike.coe, Finset.sum, Neg.neg, Polynomial.shiftedLegendre