awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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') =
    0
have h₁ : Eq.{u_3 + 1} (α := A)
  (∑ i ∈ range q,
    eval r
      ((q.choose (i + 1) * q.descFactorial (q - (i + 1))) •
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (i + 1))) *
        (⇑derivative : (a : A[X]) → A[X])^[i + 1] p'))
  0
Tactic: rw [eval_finsetSum]
-- 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)
⊢ Eq.{u_3 + 1} (α := A)
    (∑ i ∈ range q,
      eval r
        ((q.choose (i + 1) * q.descFactorial (q - (i + 1))) •
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - (q - (i + 1))) *
          (⇑derivative : (a : A[X]) → A[X])^[i + 1] p'))
    0
have h₁ : ∀ x ∈ range q,
  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: apply sum_eq_zero
-- 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
⊢ 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₁ : 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
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]
-- 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
⊢ 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₂ : 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
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]
-- 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
⊢ 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₃ : 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
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]
-- 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
⊢ 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))) •
      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
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]
-- 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
⊢ 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))) •
      (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
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]
-- 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
⊢ 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))) •
      ((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
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]
-- 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 k : ℕ
hk : q ≤ k
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - k ∧
      ∀ (r : A),
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have obtain : ∀ (p' : R[X]) (p'_le : p'.natDegree ≤ p.natDegree - k) (hp' : (⇑derivative : (a : R[X]) → R[X])^[k] p = k ! • p'),
  ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - k ∧
      ∀ (r : A),
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
Tactic: obtain ⟨p', p'_le, hp'⟩ := exists_iterate_derivative_eq_factorial_smul p 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 k : ℕ
hk : q ≤ k
p' : R[X]
p'_le : p'.natDegree ≤ p.natDegree - k
hp' : (⇑derivative : (a : R[X]) → R[X])^[k] p = k ! • p'
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - k ∧
      ∀ (r : A),
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have obtain : ∀ (k : ℕ) (hk : q ≤ q + k) (p'_le : p'.natDegree ≤ p.natDegree - (q + k))
  (hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'),
  ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - (q + k) ∧
      ∀ (r : A),
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hk
Cleared hypotheses: k, hk, p'_le, hp'
-- 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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - (q + k) ∧
      ∀ (r : A),
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
have refine : ∀ (r : A),
  (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
Tactic: refine ⟨((q + k).descFactorial k : R[X]) * p', (natDegree_C_mul_le _ _).trans p'_le, fun r => ?_⟩
-- 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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
r : A
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
have simp_rw : (aeval r : (a : R[X]) → A) ((q + k)! • p') =
  HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
Tactic: simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- 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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
r : A
simp_rw :
  (aeval r : (a : R[X]) → A) ((q + k)! • p') =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
have simp_rw₁ : (aeval r : (a : R[X]) → A) ((↑(q + k)! : R[X]) * p') =
  HMul.hMul (α := A) (β := A) ((↑q ! : A) : A)
    ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
Tactic: simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- 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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
r : A
simp_rw :
  (aeval r : (a : R[X]) → A) ((q + k)! • p') =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₁ :
  (aeval r : (a : R[X]) → A) ((↑(q + k)! : R[X]) * p') =
    HMul.hMul (α := A) (β := A) ((↑q ! : A) : A)
      ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
have simp_rw₂ : HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑(q + k)! : R[X]) : A) ((aeval r : (a : R[X]) → A) p' : A) =
  (↑q ! : A) *
    HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑((q + k).descFactorial k) : R[X]) : A)
      ((aeval r : (a : R[X]) → A) p' : A)
Tactic: simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
-- 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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative : (a : R[X]) → R[X])^[q + k] p = (q + k)! • p'
r : A
simp_rw :
  (aeval r : (a : R[X]) → A) ((q + k)! • p') =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₁ :
  (aeval r : (a : R[X]) → A) ((↑(q + k)! : R[X]) * p') =
    HMul.hMul (α := A) (β := A) ((↑q ! : A) : A)
      ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
simp_rw₂ :
  HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑(q + k)! : R[X]) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    (↑q ! : A) *
      HMul.hMul (α := A) (β := A) ((aeval r : (a : R[X]) → A) (↑((q + k).descFactorial k) : R[X]) : A)
        ((aeval r : (a : R[X]) → A) p' : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q + k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((↑((q + k).descFactorial k) : R[X]) * p') : A)
have simp_rw₃ : HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
  (↑q ! : A) * HMul.hMul (α := A) (β := A) ((↑((q + k).descFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
Tactic: simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul,
    Nat.add_descFactorial_eq_ascFactorial, Nat.factorial_mul_ascFactorial]