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
p : R[X]
q k : ℕ
hk : q ≤ k
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)
⊢ ∃ (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

Premises used: Polynomial.exists_iterate_derivative_eq_factorial_smul
-- 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 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'
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)
⊢ ∃ (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 ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hk

Premises used: Nat.exists_eq_add_of_le, rfl
-- 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 : ℕ
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)

Tactic:
⟨((q + k).descFactorial k : R[X]) * p', (natDegree_C_mul_le _ _).trans p'_le, fun r => ?_⟩

Premises used: HMul.hMul, Polynomial.natDegree_C_mul_le, Nat.cast, HAdd.hAdd, And.intro, Exists.intro, LE.le.trans, Nat.descFactorial
-- 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 : ℕ
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'
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)
⊢ ∃ (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:
refine ⟨((q + k).descFactorial k : R[X]) * p', (natDegree_C_mul_le _ _).trans p'_le, fun r => ?_⟩
-- 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 : ℕ
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)
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)
simp_rw₄ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    HMul.hMul (β := A) (HMul.hMul (α := A) (↑q ! : A) (↑((q + k).descFactorial k) : A))
      ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₅ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    HMul.hMul (α := A) (β := A) ((↑(q ! * (q + k).descFactorial k) : A) : A) ((aeval r : (a : R[X]) → A) p' : A)
simp_rw₆ :
  HMul.hMul (α := A) (β := A) ((↑(q + k)! : A) : A) ((aeval r : (a : R[X]) → A) p' : A) =
    HMul.hMul (α := A) (β := A) ((↑(q ! * (q + 1).ascFactorial k) : A) : 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)

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]

Premises used: Nat.factorial_mul_ascFactorial, mul_assoc, map_mul, Nat.cast_mul, map_natCast, nsmul_eq_mul, Nat.add_descFactorial_eq_ascFactorial
-- 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]
r : A
rw :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
rw₁ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.id A) r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))
rw₂ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.id A) r (map (algebraMap R A) ((sumIDeriv : (a : R[X]) → R[X]) p))
rw₃ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (RingHom.comp (RingHom.id A) (algebraMap R A)) r ((sumIDeriv : (a : R[X]) → R[X]) p)
rw₄ rw₅ :
  eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p) =
    eval₂ (algebraMap R A) r ((sumIDeriv : (a : R[X]) → R[X]) p)
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
    eval r ((sumIDeriv : (a : A[X]) → A[X]) (map (algebraMap R A) p))

Tactic:
rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]

Premises used: Polynomial.eval, Polynomial.sumIDeriv_map, Polynomial.eval₂_map, Polynomial.aeval_def, RingHom.id_comp
-- 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 k : ℕ
hk : k < q
h :
  natDegree.{u_1} (R := R) 0 ≤ p.natDegree - q ∧
    ∀ (r : A),
      HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (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:
use 0
-- 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 k : ℕ
hk : k < q
right :
  ∀ (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
        HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
⊢ 0 ≤ p.natDegree - q ∧
    ∀ (r : A),
      HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
        (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
          HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)

Tactic:
use Nat.zero_le _

Premises used: Nat.zero_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 k : ℕ
hk : k < q
r : A
right :
  ∀ (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])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
⊢ HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)

Tactic:
⟨p', 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
p : R[X]
q k : ℕ
hk : k < 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'
right : (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) = HSMul.hSMul (β := A) q ! 0
right₁ : Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) : A) (0 : A)
right₂ right₃ : Eq.{u_3 + 1} (α := A) 0 0
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)

Tactic:
rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]

Premises used: smul_zero, map_zero, Polynomial.aeval_iterate_derivative_of_lt
-- 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 k : ℕ
hk : q ≤ k
inr :
  ∀ (gp : R[X]) (gp_le : gp.natDegree ≤ p.natDegree - k)
    (h :
      ∀ (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)),
    ∃ (gp : R[X]),
      gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A),
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
            (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)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (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 ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk

Premises used: Polynomial.aeval_iterate_derivative_of_ge
-- 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 k : ℕ
hk : q ≤ k
gp : R[X]
gp_le : gp.natDegree ≤ p.natDegree - k
h :
  ∀ (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)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (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:
⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩

Premises used: tsub_le_tsub_left, And.intro, Exists.intro, 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 k : ℕ
hk : q ≤ k
gp : R[X]
gp_le : gp.natDegree ≤ p.natDegree - k
h :
  ∀ (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)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (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:
exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩
-- 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 k : ℕ
⊢ k < q ∨ q ≤ k

Tactic:
cases lt_or_ge k q with
    | inl hk =>
      use 0
      rw [natDegree_zero]
      use Nat.zero_le _
      intro r ⟨p', hp⟩
      rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
    | inr hk =>
      obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
      exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩

Premises used: Nat.zero_le, smul_zero, map_zero, Polynomial.natDegree_zero, lt_or_ge
-- 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 : ℕ
⊢ ∀ (k : ℕ),
    ∃ (gp : R[X]),
      gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A),
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
            (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:
have h (k) :
      ∃ gp : R[X], gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A), (X - C r) ^ q ∣ p.map (algebraMap R A) →
          aeval r (derivative^[k] p) = q ! • aeval r gp := by
    cases lt_or_ge k q with
    | inl hk =>
      use 0
      rw [natDegree_zero]
      use Nat.zero_le _
      intro r ⟨p', hp⟩
      rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
    | inr hk =>
      obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
      exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩
-- 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 : ℕ
h :
  ∀ (k : ℕ),
    ∃ (gp : R[X]),
      gp.natDegree ≤ p.natDegree - q ∧
        ∀ (r : A),
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
            (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)
choose :
  ∀ (c : (k : ℕ) → R[X])
    (h :
      ∀ (k : ℕ),
        (c k).natDegree ≤ p.natDegree - q ∧
          ∀ (r : A),
            HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
              (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),
          HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
            (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)

Tactic:
choose c h using 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 : ℕ
c : (k : ℕ) → R[X]
h :
  ∀ (k : ℕ),
    (c k).natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (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)
⊢ ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q

Tactic:
choose c_le hc using 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 : ℕ
c : (k : ℕ) → R[X]
h :
  ∀ (k : ℕ),
    (c k).natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (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)
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
⊢ ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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)

Tactic:
choose c_le hc using 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 : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)

Tactic:
⟨(range (p.natDegree + 1)).sum c, ?_, ?_⟩

Premises used: Finset.range, 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
p : R[X]
q : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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)
refine_1 : ((range (p.natDegree + 1)).sum c).natDegree ≤ p.natDegree - q
refine_2 :
  ∀ (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
        HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((range (p.natDegree + 1)).sum c) : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A),
        HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
          (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
            HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)

Tactic:
refine ⟨(range (p.natDegree + 1)).sum c, ?_, ?_⟩
-- 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 : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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)
⊢ ((range (p.natDegree + 1)).sum c).natDegree ≤ 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
p : R[X]
q : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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)
refine_1 : fold max 0 (natDegree ∘ c) (range (p.natDegree + 1)) ≤ p.natDegree - q
⊢ ((range (p.natDegree + 1)).sum c).natDegree ≤ 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
p : R[X]
q : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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)
refine_1 : 0 ≤ p.natDegree - q ∧ ∀ x ∈ range (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q
⊢ fold max 0 (natDegree ∘ c) (range (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
p : R[X]
q : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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 ∈ range (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q

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

Premises used: Nat.zero_le, And.intro
-- 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 : ℕ
c : (k : ℕ) → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc :
  ∀ (k : ℕ) (r : A),
    HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ q ∣ map (algebraMap R A) p →
      (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 ∈ range (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q

Tactic:
exact ⟨Nat.zero_le _, fun i _ => c_le i⟩