awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p' →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)

Tactic:
⟨∑ x ∈ Ico q (p.natDegree + 1), c x, ?_, ?_⟩

Premises used: Finset.Ico, HAdd.hAdd, And.intro, Exists.intro, Polynomial.natDegree, OfNat.ofNat, Finset.sum
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
inr : natDegree.{u_1} (R := R) (∑ x ∈ Ico q (p.natDegree + 1), c x) ≤ p.natDegree - q
inr₁ :
  ∀ (r : A) {p' : A[X]},
    map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p' →
      (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
        (q - 1)! • eval r p' +
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (∑ x ∈ Ico q (p.natDegree + 1), c x) : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p' →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)

Tactic:
refine ⟨∑ x ∈ Ico q (p.natDegree + 1), c x, ?_, ?_⟩
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
⊢ natDegree.{u_1} (R := R) (∑ x ∈ Ico q (p.natDegree + 1), c x) ≤ p.natDegree - q

Tactic:
(natDegree_sum_le _ _).trans ?_

Premises used: Polynomial.natDegree_sum_le, 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
inr : fold max 0 (natDegree ∘ c) (Ico q (p.natDegree + 1)) ≤ p.natDegree - q
⊢ natDegree.{u_1} (R := R) (∑ x ∈ Ico q (p.natDegree + 1), c x) ≤ p.natDegree - q

Tactic:
refine (natDegree_sum_le _ _).trans ?_

Premises used: Polynomial.natDegree_sum_le, 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
inr : 0 ≤ p.natDegree - q ∧ ∀ x ∈ Ico q (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q
⊢ fold max 0 (natDegree ∘ c) (Ico q (p.natDegree + 1)) ≤ p.natDegree - q

Tactic:
rw [fold_max_le]

Premises used: Finset.fold_max_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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
⊢ 0 ≤ p.natDegree - q ∧ ∀ x ∈ Ico q (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q

Tactic:
⟨Nat.zero_le _, fun i hi => (c_le i).trans (tsub_le_tsub_left (mem_Ico.mp hi).1 _)⟩

Premises used: Nat.zero_le, tsub_le_tsub_left, And.left, And.intro, Iff.mp, LE.le.trans, Polynomial.natDegree, Finset.mem_Ico
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
⊢ 0 ≤ p.natDegree - q ∧ ∀ x ∈ Ico q (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q

Tactic:
exact ⟨Nat.zero_le _, fun i hi => (c_le i).trans (tsub_le_tsub_left (mem_Ico.mp hi).1 _)⟩
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
rw : q ≤ p.natDegree + 1
⊢ range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)

Tactic:
rw [range_eq_Ico, range_eq_Ico, Ico_union_Ico_eq_Ico hq.le]

Premises used: LT.lt.le, Finset.Ico_union_Ico_eq_Ico, Finset.range_eq_Ico
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
rw : q - 1 ≤ p.natDegree
⊢ q ≤ p.natDegree + 1

Tactic:
rw [← tsub_le_iff_right]

Premises used: tsub_le_iff_right
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
⊢ q - 1 ≤ q - 1 + p'.natDegree

Tactic:
le_self_add

Premises used: le_self_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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
hp₁ : HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) ≠ 0
hq₁ : p' ≠ 0
⊢ q - 1 + p'.natDegree = natDegree (map (algebraMap R A) p)

Tactic:
rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]

Premises used: Polynomial.natDegree_mul, Nat.sub_add_comm, Nat.one_le_of_lt, Polynomial.natDegree_X_sub_C, Polynomial.natDegree_pow, mul_one
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
⊢ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) ≠ 0

Tactic:
pow_ne_zero _ (X_sub_C_ne_zero r)

Premises used: pow_ne_zero, Polynomial.X_sub_C_ne_zero
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
⊢ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) ≠ 0

Tactic:
exact pow_ne_zero _ (X_sub_C_ne_zero r)

Premises used: pow_ne_zero, Polynomial.X_sub_C_ne_zero
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
r : A
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * 0
⊢ p = 0

Tactic:
rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp

Premises used: MulZeroClass.mul_zero, Polynomial.map_eq_zero_iff
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
r : A
hp : p = 0
⊢ False

Tactic:
p0 hp
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
r : A
hp : p = 0
⊢ False

Tactic:
exact p0 hp
-- 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
⊢ natDegree (map (algebraMap R A) p) ≤ p.natDegree

Tactic:
natDegree_map_le

Premises used: Polynomial.natDegree_map_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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
q₁ : q - 1 + p'.natDegree = natDegree (map (algebraMap R A) p)
⊢ q - 1 ≤ p.natDegree

Tactic:
calc
      q - 1 ≤ q - 1 + p'.natDegree := le_self_add
      _ = (p.map <| algebraMap R A).natDegree := by
        rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
        · exact pow_ne_zero _ (X_sub_C_ne_zero r)
        · rintro rfl
          rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp
          exact p0 hp
      _ ≤ p.natDegree := natDegree_map_le

Premises used: Algebra.algebraMap, Polynomial.natDegree_map_le, Polynomial.map, Polynomial.natDegree, le_self_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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (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))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ 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) (c k) : A)
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 - 1) * p'
⊢ range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)

Tactic:
have : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1) := by
    rw [range_eq_Ico, range_eq_Ico, Ico_union_Ico_eq_Ico hq.le]
    rw [← tsub_le_iff_right]
    calc
      q - 1 ≤ q - 1 + p'.natDegree := le_self_add
      _ = (p.map <| algebraMap R A).natDegree := by
        rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
        · exact pow_ne_zero _ (X_sub_C_ne_zero r)
        · rintro rfl
          rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp
          exact p0 hp
      _ ≤ p.natDegree := natDegree_map_le