-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q * p'
k : ℕ
hk : k < q
h :
  ∀ (x : ℕ),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x)) =
      HPow.hPow (β := ℕ) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) 1 *
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x) - 1)
simp_rw :
  eval r
      ((⇑derivative : (a : A[X]) → A[X])^[k]
        (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q * p')) =
    0
simp_rw₁ :
  eval r
      (∑ k_1 ∈ range k.succ,
        k.choose k_1 •
          ((⇑derivative : (a : A[X]) → A[X])^[k - k_1]
              (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q) *
            (⇑derivative : (a : A[X]) → A[X])^[k_1] p')) =
    0
simp_rw₂ :
  eval r
      (∑ x ∈ range k.succ,
        k.choose x •
          (q.descFactorial (k - x) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x)) *
            (⇑derivative : (a : A[X]) → A[X])^[x] p')) =
    0
simp_rw₃ :
  eval r
      (∑ x ∈ range k.succ,
        k.choose x •
            q.descFactorial (k - x) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x)) *
          (⇑derivative : (a : A[X]) → A[X])^[x] p') =
    0
simp_rw₄ :
  eval r
      (∑ x ∈ range k.succ,
        (k.choose x * q.descFactorial (k - x)) •
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x)) *
          (⇑derivative : (a : A[X]) → A[X])^[x] p') =
    0
simp_rw₅ :
  eval r
      (∑ x ∈ range k.succ,
        (k.choose x * q.descFactorial (k - x)) •
            (HPow.hPow (β := ℕ) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) 1 *
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x) - 1)) *
          (⇑derivative : (a : A[X]) → A[X])^[x] p') =
    0
simp_rw₆ :
  eval r
      (∑ x ∈ range k.succ,
        HPow.hPow (β := ℕ) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) 1 *
            (k.choose x * q.descFactorial (k - x)) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x) - 1) *
          (⇑derivative : (a : A[X]) → A[X])^[x] p') =
    0
simp_rw₇ :
  eval r
      (∑ x ∈ range k.succ,
        HPow.hPow (β := ℕ) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) 1 *
          ((k.choose x * q.descFactorial (k - x)) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - x) - 1) *
            (⇑derivative : (a : A[X]) → A[X])^[x] p')) =
    0
simp_rw₈ :
  eval r
      (HPow.hPow (β := ℕ) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) 1 *
        ∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - i) - 1) *
            (⇑derivative : (a : A[X]) → A[X])^[i] p') =
    0
simp_rw₉ :
  eval r (HPow.hPow (β := ℕ) (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) 1) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - i) - 1) *
            (⇑derivative : (a : A[X]) → A[X])^[i] p') =
    0
simp_rw₁₀ :
  eval r (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - i) - 1) *
            (⇑derivative : (a : A[X]) → A[X])^[i] p') =
    0
simp_rw₁₁ :
  (eval r X - eval r ((C : (a : A) → A[X]) r)) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - i) - 1) *
            (⇑derivative : (a : A[X]) → A[X])^[i] p') =
    0
simp_rw₁₂ :
  (r - eval r ((C : (a : A) → A[X]) r)) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - i) - 1) *
            (⇑derivative : (a : A[X]) → A[X])^[i] p') =
    0
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have simp_rw₁₃ : (r - r) *
    eval r
      (∑ i ∈ range k.succ,
        (k.choose i * q.descFactorial (k - i)) •
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (k - i) - 1) *
          (⇑derivative : (a : A[X]) → A[X])^[i] p') =
  0
Tactic: simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul,
    h, ← mul_smul_comm, mul_assoc, ← mul_sum, eval_mul, pow_one, eval_sub, eval_X, eval_C, sub_self,
    zero_mul]