awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k : ℕ
⊢ 0 ≤ p.natDegree - k ∧
    ∀ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree
          (fun (i : ℕ) ↦
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
              (HPow.hPow (α := R[X]) X i))
          x ≤
        p.natDegree - k
have refine : ∀ (i : ℕ) (hi : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support),
  Function.comp.{1, u_1 + 1, 1} (β := R[X]) natDegree
      (fun (i : ℕ) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
          (HPow.hPow (α := R[X]) X i))
      i ≤
    p.natDegree - k
Tactic: refine ⟨Nat.zero_le _, fun i hi => ?_⟩
-- 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
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)
have rw : 1 ≤ q - (k - x)
Tactic: rw [← pow_add, add_tsub_cancel_of_le]
-- 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
x : ℕ
⊢ 1 ≤ q - (k - x)
have rw : ∀ (hk : k + 1 ≤ q) (x : ℕ), 1 ≤ q - (k - x)
Tactic: rw [Nat.lt_iff_add_one_le] at hk
Cleared hypotheses: hk, x
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) : A) (0 : A)
have 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)
Tactic: have h (x) : (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1) := by
    rw [← pow_add, add_tsub_cancel_of_le]
    rw [Nat.lt_iff_add_one_le] at hk
    exact (le_tsub_of_add_le_left hk).trans (tsub_le_tsub_left (tsub_le_self : _ ≤ k) _)
-- 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)
⊢ Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) : A) (0 : A)
have rw : eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
Tactic: rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]
-- 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)
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have 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
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]
-- 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
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have 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
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]
-- 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
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have 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
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]
-- 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
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have 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
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]
-- 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
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have 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
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]
-- 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
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have 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
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]
-- 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
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
have 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
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]
-- 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'
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)
have rw : 1 ≤ q - (q - x)
Tactic: rw [← pow_add, add_tsub_cancel_of_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
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'
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q] p) = q ! • eval r p'
have 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)
Tactic: have h (x) (h : 1 ≤ x) (h' : x ≤ q) :
      (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1) := by
    rw [← pow_add, add_tsub_cancel_of_le]
    rwa [tsub_tsub_cancel_of_le h']
-- 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)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q] p) = q ! • eval r p'
have rw : eval r ((⇑derivative : (a : A[X]) → A[X])^[q] (map (algebraMap R A) p)) = q ! • eval r p'
Tactic: rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]
-- 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)
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[q] (map (algebraMap R A) p)) = q ! • eval r p'
have simp_rw : eval r
    (∑ x ∈ range q.succ,
      (q.choose x * q.descFactorial (q - x)) •
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - x)) *
        (⇑derivative : (a : A[X]) → A[X])^[x] p') =
  q ! • eval r p'
Tactic: simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul]
-- 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)
⊢ eval r
      (∑ x ∈ range q.succ,
        (q.choose x * q.descFactorial (q - x)) •
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - x)) *
          (⇑derivative : (a : A[X]) → A[X])^[x] p') =
    q ! • eval r p'
have rw : eval r
      (∑ k ∈ range q,
        (q.choose (k + 1) * q.descFactorial (q - (k + 1))) •
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (k + 1))) *
          (⇑derivative : (a : A[X]) → A[X])^[k + 1] p') +
    q ! • eval r p' =
  q ! • eval r p'
Tactic: rw [sum_range_succ', Nat.choose_zero_right, one_mul, tsub_zero, Nat.descFactorial_self, tsub_self,
    pow_zero, smul_mul_assoc, one_mul, Function.iterate_zero_apply, eval_add, eval_smul]
-- 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)
⊢ eval r
        (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) •
              HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (k + 1))) *
            (⇑derivative : (a : A[X]) → A[X])^[k + 1] p') +
      q ! • eval r p' =
    q ! • eval r p'
have h₁ : eval r
    (∑ k ∈ range q,
      (q.choose (k + 1) * q.descFactorial (q - (k + 1))) •
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (k + 1))) *
        (⇑derivative : (a : A[X]) → A[X])^[k + 1] p') =
  0
Tactic: convert! zero_add _