awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
rw :
  ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
    map f ((sumIDeriv : (a : R[X]) → R[X]) p)
⊢ (sumIDeriv : (a : S[X]) → S[X]) (map f p) = map f ((sumIDeriv : (a : R[X]) → R[X]) p)

Tactic:
rw [sumIDeriv_apply_of_le (le_max_left _ _ : _ ≤ n)]

Premises used: Polynomial.sumIDeriv_apply_of_le, le_max_left
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
rw :
  ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
    map f (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : R[X]) → R[X])^[i] p)
⊢ ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
    map f ((sumIDeriv : (a : R[X]) → R[X]) p)

Tactic:
rw [sumIDeriv_apply_of_le (le_max_right _ _ : _ ≤ n)]

Premises used: le_max_right, Polynomial.sumIDeriv_apply_of_le
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max (map f p).natDegree p.natDegree
simp_rw :
  Eq.{u_2 + 1} (α := S[X])
    (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p))
    (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), map f ((⇑derivative : (a : R[X]) → R[X])^[i] p))
⊢ ∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : S[X]) → S[X])^[i] (map f p) =
    map f (∑ i ∈ range (max (map f p).natDegree p.natDegree + 1), (⇑derivative : (a : R[X]) → R[X])^[i] p)

Tactic:
simp_rw [Polynomial.map_sum, iterate_derivative_map p f]

Premises used: Polynomial.map_sum, Polynomial.iterate_derivative_map
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw :
  Eq.{u_1 + 1} (α := R[X])
    (∑ i ∈ range (p.natDegree + 1), (⇑derivative : (a : R[X]) → R[X])^[i] ((derivative : (a : R[X]) → R[X]) p))
    (∑ b ∈ range (p.natDegree + 1), (derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[b] p))
⊢ Eq (α := R[X]) ((sumIDeriv : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p) : R[X])
    ((derivative : (a : R[X]) → R[X]) ((sumIDeriv : (a : R[X]) → R[X]) p) : R[X])

Tactic:
rw [sumIDeriv_apply_of_le ((natDegree_derivative_le p).trans tsub_le_self), sumIDeriv_apply,
    derivative_sum]

Premises used: Polynomial.derivative_sum, Polynomial.natDegree_derivative_le, Polynomial.sumIDeriv_apply, tsub_le_self, LE.le.trans, Polynomial.sumIDeriv_apply_of_le
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
rw :
  (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      HAdd.hAdd (α := R[X]) (β := R[X])
        (∑ x ∈ range p.natDegree, (derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : R[X])
        ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[p.natDegree] p) : R[X])
⊢ (sumIDeriv : (a : R[X]) → R[X]) p =
    HAdd.hAdd (β := R[X]) p ((derivative : (a : R[X]) → R[X]) ((sumIDeriv : (a : R[X]) → R[X]) p) : R[X])

Tactic:
rw [sumIDeriv_apply, derivative_sum, sum_range_succ', sum_range_succ,
    add_comm, ← add_zero (Finset.sum _ _)]

Premises used: Polynomial.derivative_sum, add_comm, Polynomial.sumIDeriv_apply, add_zero, Finset.sum_range_succ', Finset.sum_range_succ, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
simp_rw :
  (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      (∑ x ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[x.succ] p +
        (⇑derivative : (a : R[X]) → R[X])^[p.natDegree.succ] p)
simp_rw₁ :
  (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p +
        (⇑derivative : (a : R[X]) → R[X])^[p.natDegree + 1] p)
simp_rw₂ :
  p + HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p +
        (⇑derivative : (a : R[X]) → R[X])^[p.natDegree + 1] p)
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] p +
      HAdd.hAdd (α := R[X]) (∑ k ∈ range p.natDegree, (⇑derivative : (a : R[X]) → R[X])^[k + 1] p) 0 =
    p +
      HAdd.hAdd (α := R[X]) (β := R[X])
        (∑ x ∈ range p.natDegree, (derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : R[X])
        ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[p.natDegree] p) : R[X])

Tactic:
simp_rw [← Function.iterate_succ_apply' derivative, Nat.succ_eq_add_one,
    Function.iterate_zero_apply, iterate_derivative_eq_zero (Nat.lt_succ_self _)]

Premises used: Polynomial.derivative, Function.iterate_succ_apply', Nat.succ_eq_add_one, Nat.lt_succ_self, Polynomial.iterate_derivative_eq_zero, Function.iterate_zero_apply, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k : ℕ
⊢ ∃ (gp : R[X]), gp.natDegree ≤ p.natDegree - k ∧ (⇑derivative : (a : R[X]) → R[X])^[k] p = k ! • gp

Tactic:
⟨_, (natDegree_sum_le _ _).trans ?_, iterate_derivative_eq_factorial_smul_sum p k⟩

Premises used: Polynomial.iterate_derivative_eq_factorial_smul_sum, Polynomial.natDegree_sum_le, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k : ℕ
refine :
  fold max 0
      (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))
      ((⇑derivative : (a : R[X]) → R[X])^[k] p).support ≤
    p.natDegree - k
⊢ ∃ (gp : R[X]), gp.natDegree ≤ p.natDegree - k ∧ (⇑derivative : (a : R[X]) → R[X])^[k] p = k ! • gp

Tactic:
refine ⟨_, (natDegree_sum_le _ _).trans ?_, iterate_derivative_eq_factorial_smul_sum p k⟩
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k : ℕ
rw :
  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
⊢ fold max 0
      (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))
      ((⇑derivative : (a : R[X]) → R[X])^[k] p).support ≤
    p.natDegree - k

Tactic:
rw [fold_max_le]

Premises used: Finset.fold_max_le
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
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

Tactic:
⟨Nat.zero_le _, fun i hi => ?_⟩

Premises used: Nat.zero_le, And.intro
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k : ℕ
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
⊢ 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

Tactic:
refine ⟨Nat.zero_le _, fun i hi => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k i : ℕ
hi : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
⊢ (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)).natDegree ≤
    p.natDegree - k

Tactic:
(natDegree_C_mul_le _ _).trans <| (natDegree_X_pow_le _).trans <|
    (le_natDegree_of_mem_supp _ hi).trans <| natDegree_iterate_derivative _ _

Premises used: Polynomial.le_natDegree_of_mem_supp, Polynomial.natDegree_C_mul_le, Polynomial.natDegree_X_pow_le, LE.le.trans, Polynomial.natDegree_iterate_derivative
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
k i : ℕ
hi : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
⊢ (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)).natDegree ≤
    p.natDegree - k

Tactic:
exact (natDegree_C_mul_le _ _).trans <| (natDegree_X_pow_le _).trans <|
    (le_natDegree_of_mem_supp _ hi).trans <| natDegree_iterate_derivative _ _

Premises used: Polynomial.le_natDegree_of_mem_supp, Polynomial.natDegree_C_mul_le, Polynomial.natDegree_X_pow_le, LE.le.trans, Polynomial.natDegree_iterate_derivative
-- 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'
k : ℕ
hk : k < q
x : ℕ
rw : 1 ≤ q - (k - 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:
rw [← pow_add, add_tsub_cancel_of_le]

Premises used: pow_add, add_tsub_cancel_of_le
-- 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'
k : ℕ
hk : k < q
x : ℕ
rw : ∀ (hk : k + 1 ≤ q) (x : ℕ), 1 ≤ q - (k - x)
⊢ 1 ≤ q - (k - x)

Tactic:
rw [Nat.lt_iff_add_one_le] at hk

Premises used: Nat.lt_iff_add_one_le
-- 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'
k : ℕ
hk : k + 1 ≤ q
x : ℕ
⊢ 1 ≤ q - (k - x)

Tactic:
(le_tsub_of_add_le_left hk).trans (tsub_le_tsub_left (tsub_le_self : _ ≤ k) _)

Premises used: le_tsub_of_add_le_left, tsub_le_tsub_left, tsub_le_self, LE.le.trans
-- 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'
k : ℕ
hk : k + 1 ≤ q
x : ℕ
⊢ 1 ≤ q - (k - x)

Tactic:
exact (le_tsub_of_add_le_left hk).trans (tsub_le_tsub_left (tsub_le_self : _ ≤ k) _)

Premises used: le_tsub_of_add_le_left, tsub_le_tsub_left, tsub_le_self, LE.le.trans
-- 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'
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)

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) _)
-- 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'
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)
rw : eval r ((⇑derivative : (a : A[X]) → A[X])^[k] (map (algebraMap R A) p)) = 0
⊢ Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) : A) (0 : A)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]

Premises used: Polynomial.aeval_def, Polynomial.iterate_derivative_map, Polynomial.eval₂_eq_eval_map
-- 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'
x : ℕ
h : 1 ≤ x
h' : x ≤ q
rw : 1 ≤ q - (q - x)
⊢ 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:
rw [← pow_add, add_tsub_cancel_of_le]

Premises used: pow_add, add_tsub_cancel_of_le
-- 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'
x : ℕ
h : 1 ≤ x
h' : x ≤ q
rwa rwa₁ rwa₂ rwa₃ : 1 ≤ x
⊢ 1 ≤ q - (q - x)

Tactic:
rwa [tsub_tsub_cancel_of_le h']

Premises used: tsub_tsub_cancel_of_le
-- 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'
⊢ ∀ (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']
-- 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)
rw : eval r ((⇑derivative : (a : A[X]) → A[X])^[q] (map (algebraMap R A) p)) = q ! • eval r p'
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q] p) = q ! • eval r p'

Tactic:
rw [aeval_def, eval₂_eq_eval_map, ← iterate_derivative_map]

Premises used: Polynomial.aeval_def, Polynomial.iterate_derivative_map, Polynomial.eval₂_eq_eval_map
-- 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)
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'
⊢ eval r ((⇑derivative : (a : A[X]) → A[X])^[q] (map (algebraMap R A) p)) = q ! • eval r p'

Tactic:
simp_rw [hp, iterate_derivative_mul, iterate_derivative_X_sub_pow, ← smul_mul_assoc, smul_smul]

Premises used: Polynomial.iterate_derivative_X_sub_pow, smul_smul, smul_mul_assoc, Polynomial.iterate_derivative_mul
-- 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)
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'
⊢ 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:
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]

Premises used: tsub_self, smul_mul_assoc, pow_zero, tsub_zero, Polynomial.eval_add, Nat.descFactorial_self, Polynomial.eval_smul, Function.iterate_zero_apply, Finset.sum_range_succ', Nat.choose_zero_right, one_mul
-- 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)
⊢ 0 + q ! • eval r p' = q ! • eval r p'

Tactic:
zero_add _

Premises used: zero_add
-- 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)
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
⊢ 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:
convert! zero_add _

Premises used: zero_add
-- 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)
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
⊢ 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:
rw [eval_finsetSum]

Premises used: Polynomial.eval_finsetSum
-- 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)
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
⊢ 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:
apply sum_eq_zero

Premises used: Finset.sum_eq_zero