awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
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
⊢ ∃ (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)
have 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)
Tactic: refine ⟨(range (p.natDegree + 1)).sum c, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
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
have refine_1 : fold max 0 (natDegree ∘ c) (range (p.natDegree + 1)) ≤ p.natDegree - q
Tactic: refine (natDegree_sum_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
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)
⊢ fold max 0 (natDegree ∘ c) (range (p.natDegree + 1)) ≤ p.natDegree - q
have refine_1 : 0 ≤ p.natDegree - q ∧ ∀ x ∈ range (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q
Tactic: rw [fold_max_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
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
⊢ 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)
have 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)
Tactic: ⟨p', hp⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
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'
⊢ (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)
have 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)
Tactic: rw [sumIDeriv_apply, map_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
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'
⊢ ∑ 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)
have 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)
Tactic: simp_rw [hc _ r ⟨_, hp⟩, map_sum, smul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
p : R[X]
q : ℕ
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)
⊢ ∑ 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)
have 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))
Tactic: simp_rw [hc _ r ⟨_, hp⟩, map_sum, smul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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)
⊢ ∃ (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)
have 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)
Tactic: rcases eq_or_ne p 0 with (rfl | p0)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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)
⊢ ∃ (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)
have 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)
Tactic: rcases eq_or_ne p 0 with (rfl | p0)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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)
⊢ ∃ (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)
have 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)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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)
⊢ 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)
have 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)
Tactic: use Nat.zero_le _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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'
⊢ (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)
have right : 0 = (q - 1)! • eval r p'
Tactic: rw [map_zero, map_zero, smul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
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 = (q - 1)! • eval r p'
have hp₁ : 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
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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'
⊢ 0 = (q - 1)! • eval r p'
have right : ∀ (hp : p' = 0), 0 = (q - 1)! • eval r p'
Tactic: replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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'
⊢ 0 = (q - 1)! • eval r p'
have right₁ : ¬HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) = 0
Tactic: replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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
⊢ 0 = (q - 1)! • eval r p'
have right : 0 = (q - 1)! • eval r 0
Tactic: rw [hp, eval_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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
⊢ 0 = (q - 1)! • eval r p'
have right₁ : 0 = HSMul.hSMul (β := A) (q - 1)! 0
Tactic: rw [hp, eval_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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
⊢ 0 = (q - 1)! • eval r p'
have right₂ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [hp, eval_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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 : ℕ
⊢ 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
have 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))
        sorry).natDegree ≤
    p.natDegree - k
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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
⊢ 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
have neg : ∀ (h : ¬q ≤ k), natDegree.{u_1} (R := R) 0 ≤ p.natDegree - k
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
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
⊢ ∃ (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)
have c_le : ∀ (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 _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
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)
have 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))
            sorry) :
        A)
Tactic: simp_rw [c, dif_pos hk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
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
⊢ ∃ (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)
have 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)
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