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
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)
have inr : natDegree.{u_1} (R := R) (∑ x ∈ Ico q (p.natDegree + 1), c x) ≤ p.natDegree - q
Tactic: refine ⟨∑ x ∈ Ico q (p.natDegree + 1), c x, ?_, ?_⟩
-- 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
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
⊢ ∃ (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₁ : ∀ (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)
Tactic: refine ⟨∑ x ∈ Ico q (p.natDegree + 1), c x, ?_, ?_⟩
-- 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
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
have inr : fold max 0 (natDegree ∘ c) (Ico q (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
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)
⊢ fold max 0 (natDegree ∘ c) (Ico q (p.natDegree + 1)) ≤ p.natDegree - q
have inr : 0 ≤ p.natDegree - q ∧ ∀ x ∈ Ico q (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
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)
have rw : q ≤ p.natDegree + 1
Tactic: rw [range_eq_Ico, range_eq_Ico, Ico_union_Ico_eq_Ico hq.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
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 ≤ p.natDegree + 1
have rw : q - 1 ≤ p.natDegree
Tactic: rw [← tsub_le_iff_right]
-- 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
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 + p'.natDegree = natDegree (map (algebraMap R A) p)
have hp₁ : HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) ≠ 0
Tactic: rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
-- 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
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
⊢ q - 1 + p'.natDegree = natDegree (map (algebraMap R A) p)
have hq₁ : p' ≠ 0
Tactic: rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
-- 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
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
⊢ False
have hp₁ : p = 0
Tactic: rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] 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
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 ≤ p.natDegree
have q₁ : q - 1 + p'.natDegree = natDegree (map (algebraMap R A) p)
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
-- 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
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'
⊢ (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)
have this : 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
-- 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
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'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ (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)
have inr : (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
  0 + (q - 1)! • eval r p' +
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (∑ x ∈ Ico q (p.natDegree + 1), c x) : A)
Tactic: rw [← zero_add ((q - 1)! • p'.eval r)]
-- 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
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'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ (aeval r : (a : R[X]) → A) ((sumIDeriv : (a : R[X]) → R[X]) p : R[X]) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (∑ x ∈ Ico q (p.natDegree + 1), c x) : A)
have inr : ∑ x ∈ range q ∪ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
  0 + (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
Tactic: rw [sumIDeriv_apply, map_sum, map_sum, this]
-- 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
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'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ range q = range (q - 1 + 1)
have rw : range q = range q
Tactic: rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]
-- 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
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'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
⊢ ∑ x ∈ range q ∪ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
have this₁ : range q = range (q - 1 + 1)
Tactic: have : range q = range (q - 1 + 1) := by rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]
-- 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
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'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∑ x ∈ range q ∪ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
have inr : HAdd.hAdd (α := A) (β := A)
      (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A)
      ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A) +
    ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
  0 + (q - 1)! • eval r p' + HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
Tactic: rw [sum_union, this, sum_range_succ]