-- 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'
h :
  ∀ (x : ℕ) (h : 1 ≤ x) (h' : x ≤ q),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - 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 - (q - x) - 1)
x : ℕ
hx : x ∈ range q
h₁ :
  eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
          (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 - (q - (x + 1)) - 1)) *
        (⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
h₂ :
  eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
          (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) *
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (x + 1)) - 1)) *
        (⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
h₃ :
  eval r
        ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
          (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) *
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
h₄ :
  (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        eval r
          (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) *
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (x + 1)) - 1)) *
      eval r ((⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
h₅ :
  (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        (eval r (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X])) *
          eval r (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
h₆ :
  (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        ((eval r X - eval r ((C : (a : A) → A[X]) r)) *
          eval r (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
⊢ eval r
      ((q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (x + 1))) *
        (⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
have h₇ : (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
      ((r - eval r ((C : (a : A) → A[X]) r)) *
        eval r (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (x + 1)) - 1))) *
    eval r ((⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
  0
Tactic: rw [h (x + 1) le_add_self (Nat.add_one_le_iff.mpr (mem_range.mp hx)), pow_one,
    eval_mul, eval_smul, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul,
    smul_zero, zero_mul]