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 : ℕ
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)
r : A
refine_2 :
  ∀ (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) ((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)
⊢ 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)

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 : ℕ
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)
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'
refine_2 :
  ∑ x ∈ range (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((range (p.natDegree + 1)).sum c) : A)
⊢ (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)

Tactic:
rw [sumIDeriv_apply, map_sum]

Premises used: map_sum, Polynomial.sumIDeriv_apply
-- 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)
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'
refine_2 :
  ∑ x ∈ range (p.natDegree + 1), HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c x) : A) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((range (p.natDegree + 1)).sum c) : A)
refine_2₁ :
  ∑ x ∈ range (p.natDegree + 1), HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c x) : A) =
    HSMul.hSMul (β := A) q ! (∑ x ∈ range (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
⊢ ∑ x ∈ range (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) ((range (p.natDegree + 1)).sum c) : A)

Tactic:
simp_rw [hc _ r ⟨_, hp⟩, map_sum, smul_sum]

Premises used: map_sum, Exists.intro, Finset.smul_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)
inl :
  ∃ (gp : R[X]),
    gp.natDegree ≤ natDegree.{u_1} (R := R) 0 - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) 0 = 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]) 0) =
            (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A)
inr :
  ∀ (p0 : p ≠ 0),
    ∃ (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)
⊢ ∃ (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:
rcases eq_or_ne p 0 with (rfl | p0)

Premises used: eq_or_ne, OfNat.ofNat, 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
h :
  natDegree.{u_1} (R := R) 0 ≤ natDegree.{u_1} (R := R) 0 - q ∧
    ∀ (r : A) {p' : A[X]},
      map (algebraMap R A) 0 = 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]) 0) =
          (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ natDegree.{u_1} (R := R) 0 - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) 0 = 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]) 0) =
            (q - 1)! • eval r 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
right :
  ∀ (r : A) {p' : A[X]},
    map (algebraMap R A) 0 = 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]) 0) =
        (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)
⊢ 0 ≤ 0 - q ∧
    ∀ (r : A) {p' : A[X]},
      map (algebraMap R A) 0 = 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]) 0) =
          (q - 1)! • eval r 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
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : A
p' : A[X]
hp : map (algebraMap R A) 0 = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
right : 0 = (q - 1)! • eval r p'
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) 0) =
    (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) 0 : A)

Tactic:
rw [map_zero, map_zero, smul_zero, add_zero]

Premises used: smul_zero, map_zero, add_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
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : A
p' : A[X]
hp : map (algebraMap R A) 0 = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
⊢ 0 = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'

Tactic:
rw [Polynomial.map_zero] at hp

Premises used: Polynomial.map_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
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : A
p' : A[X]
hp : 0 = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
right : ∀ (hp : p' = 0), 0 = (q - 1)! • eval r p'
right₁ : ¬HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) = 0
⊢ 0 = (q - 1)! • eval r p'

Tactic:
replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_
-- 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
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : A
p' : A[X]
hp : p' = 0
right : 0 = (q - 1)! • eval r 0
right₁ : 0 = HSMul.hSMul (β := A) (q - 1)! 0
right₂ right₃ : Eq.{u_3 + 1} (α := A) 0 0
⊢ 0 = (q - 1)! • eval r p'

Tactic:
rw [hp, eval_zero, smul_zero]

Premises used: smul_zero, Polynomial.eval_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
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : A
p' : A[X]
hp : 0 = 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:
fun h => X_sub_C_ne_zero r (eq_zero_of_pow_eq_zero h)

Premises used: eq_zero_of_pow_eq_zero, Polynomial.X_sub_C_ne_zero, Not
-- 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
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
r : A
p' : A[X]
hp : 0 = 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 fun h => X_sub_C_ne_zero r (eq_zero_of_pow_eq_zero h)

Premises used: eq_zero_of_pow_eq_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
k : ℕ
dsimp :
  natDegree.{u_1} (R := R)
      (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) ≤
    p.natDegree - k
⊢ (c k).natDegree ≤ p.natDegree - k

Tactic:
dsimp only [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
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
k : ℕ
pos :
  ∀ (h : q ≤ k),
    (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))
          ⋯).natDegree ≤
      p.natDegree - k
neg : ∀ (h : ¬q ≤ k), natDegree.{u_1} (R := R) 0 ≤ p.natDegree - k
⊢ natDegree.{u_1} (R := R)
      (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) ≤
    p.natDegree - k

Tactic:
split_ifs with 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
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
k : ℕ
h : q ≤ k
⊢ (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))
        ⋯).natDegree ≤
    p.natDegree - k

Tactic:
(aeval_iterate_derivative_of_ge A p q h).choose_spec.1

Premises used: Exists.choose_spec, Polynomial.aeval_iterate_derivative_of_ge, And.left
-- 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
k : ℕ
h : q ≤ k
⊢ (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))
        ⋯).natDegree ≤
    p.natDegree - k

Tactic:
exact (aeval_iterate_derivative_of_ge A p q h).choose_spec.1

Premises used: Exists.choose_spec, Polynomial.aeval_iterate_derivative_of_ge, And.left
-- 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
k : ℕ
h : ¬q ≤ k
⊢ 0 ≤ p.natDegree - k

Tactic:
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
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
k : ℕ
h : ¬q ≤ k
⊢ 0 ≤ p.natDegree - k

Tactic:
exact 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
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
⊢ ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k

Tactic:
have c_le (k) : (c k).natDegree ≤ p.natDegree - k := by
    dsimp only [c]
    split_ifs with h
    · exact (aeval_iterate_derivative_of_ge A p q h).choose_spec.1
    · rw [natDegree_zero]; exact 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
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
k : ℕ
hk : q ≤ k
simp_rw :
  ∀ (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)
            (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))
              ⋯) :
          A)
⊢ ∀ (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)

Tactic:
simp_rw [c, dif_pos hk]

Premises used: dif_pos
-- 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
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)
            (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))
              ⋯) :
          A)

Tactic:
(aeval_iterate_derivative_of_ge A p q hk).choose_spec.2

Premises used: Exists.choose_spec, Polynomial.aeval_iterate_derivative_of_ge, And.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
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)
            (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))
              ⋯) :
          A)

Tactic:
exact (aeval_iterate_derivative_of_ge A p q hk).choose_spec.2

Premises used: Exists.choose_spec, Polynomial.aeval_iterate_derivative_of_ge, And.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
⊢ ∀ (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)

Tactic:
have hc (k) (hk : q ≤ k) : ∀ (r : A), aeval r (derivative^[k] p) = q ! • aeval r (c k) := by
    simp_rw [c, dif_pos hk]
    exact (aeval_iterate_derivative_of_ge A p q hk).choose_spec.2