-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
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
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
h₈ :
  (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        ((r - 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
h₉ :
  (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        (0 * 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₁₀ :
  HSMul.hSMul (β := A) (q.choose (x + 1) * q.descFactorial (q - (x + 1))) 0 *
      eval r ((⇑derivative : (a : A[X]) → A[X])^[x + 1] p') =
    0
h₁₁ : 0 * eval r ((⇑derivative : (a : A[X]) → A[X])^[x + 1] p') = 0
h₁₂ h₁₃ : Eq.{u_3 + 1} (α := A) 0 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

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]

Premises used: Iff.mpr, Polynomial.eval_C, sub_self, Polynomial.eval_X, MulZeroClass.zero_mul, smul_zero, Polynomial.eval_mul, Finset.mem_range, Nat.add_one_le_iff, HAdd.hAdd, pow_one, Iff.mp, Polynomial.eval_smul, OfNat.ofNat, Polynomial.eval_sub, le_add_self