awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
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)
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)
⊢ (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:
rw [← zero_add ((q - 1)! • p'.eval r)]

Premises used: Polynomial.eval, HSub.hSub, zero_add, Nat.factorial, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
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))
⊢ (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 [sumIDeriv_apply, map_sum, map_sum, this]

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
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)
rw rw₁ : range q = range q
⊢ range q = range (q - 1 + 1)

Tactic:
rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]

Premises used: tsub_add_cancel_of_le, Nat.one_le_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
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)

Tactic:
have : range q = range (q - 1 + 1) := by rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
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))
inr₁ : Disjoint (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))

Tactic:
rw [sum_union, this, sum_range_succ]

Premises used: Finset.sum_union, Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
inr :
  Eq.{u_3 + 1} (α := A) (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p)) 0
inr₁ : (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) = (q - 1)! • eval r p'
inr₂ :
  ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
⊢ 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:
congr 2
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
inr :
  ∀ x ∈ range (q - 1),
    Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := A) (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p)) 0

Tactic:
apply sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∀ x ∈ range (q - 1),
    Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A) (0 : A)

Tactic:
fun x hx => aeval_iterate_derivative_of_lt p _ r hp (mem_range.mp hx)

Premises used: HSub.hSub, Finset.mem_range, Iff.mp, Polynomial.aeval_iterate_derivative_of_lt, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
⊢ ∀ x ∈ range (q - 1),
    Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A) (0 : A)

Tactic:
exact fun x hx => aeval_iterate_derivative_of_lt p _ r hp (mem_range.mp hx)

Premises used: HSub.hSub, Finset.mem_range, Iff.mp, Polynomial.aeval_iterate_derivative_of_lt, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
inr inr₁ :
  Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A)
    ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) = (q - 1)! • eval r p'

Tactic:
rw [← aeval_iterate_derivative_self _ _ _ hp]

Premises used: Polynomial.aeval_iterate_derivative_self
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
inr :
  ∀ x ∈ Ico q (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) (c x) : A)
⊢ ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))

Tactic:
rw [smul_sum, sum_congr rfl]

Premises used: Finset.smul_sum, Finset.sum_congr, 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
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)
k : ℕ
hk : k ∈ Ico q (p.natDegree + 1)
⊢ (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:
hc k (mem_Ico.mp hk).1 r

Premises used: And.left, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
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)
k : ℕ
hk : k ∈ Ico q (p.natDegree + 1)
⊢ (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:
exact hc k (mem_Ico.mp hk).1 r

Premises used: And.left, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
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)
inr : ∀ (x : ℕ), x ∉ Ico 0 q ∩ Ico q (p.natDegree + 1)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))

Tactic:
rw [range_eq_Ico, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem]

Premises used: Finset.eq_empty_iff_forall_notMem, Finset.disjoint_iff_inter_eq_empty, Finset.range_eq_Ico
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : x ∈ Ico 0 q ∩ Ico q (p.natDegree + 1)
⊢ (0 ≤ x ∧ x < q) ∧ q ≤ x ∧ x < p.natDegree + 1

Tactic:
rw [mem_inter, mem_Ico, mem_Ico] at hx

Premises used: Finset.mem_inter, Finset.mem_Ico