awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s : Multiset ι
f : ι → R[X]
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
have refine : ∀ (i : ι) (s : Multiset ι)
  (h :
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
      (Multiset.sum
          (Multiset.map
            (fun (i : ι) ↦
              HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
            s) :
        R[X])),
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f (i ::ₘ s)).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i_1 : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
              ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
          (i ::ₘ s)) :
      R[X])
Tactic: refine Multiset.induction_on s (by simp) fun i s h => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f (i ::ₘ s)).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i_1 : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
              ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
          (i ::ₘ s)) :
      R[X])
have rw : HMul.hMul (β := R[X]) (Multiset.map f s).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]) +
    HMul.hMul (β := R[X]) (f i) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X]) =
  HMul.hMul (β := R[X]) (Multiset.map f s).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]) +
    Multiset.sum
      (Multiset.map
        (fun (i_1 : ι) ↦
          HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
            ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
        s)
Tactic: rw [Multiset.map_cons, Multiset.prod_cons, derivative_mul, Multiset.map_cons _ i s,
    Multiset.sum_cons, Multiset.erase_cons_head, mul_comm (derivative (f i))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
⊢ HMul.hMul (β := R[X]) (Multiset.map f s).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]) +
      HMul.hMul (β := R[X]) (f i) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X]) =
    HMul.hMul (β := R[X]) (Multiset.map f s).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]) +
      Multiset.sum
        (Multiset.map
          (fun (i_1 : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
              ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
          s)
have e_a : HMul.hMul (β := R[X]) (f i) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X]) =
  Multiset.sum
    (Multiset.map
      (fun (i_1 : ι) ↦
        HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
          ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
      s)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
⊢ HMul.hMul (β := R[X]) (f i) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X]) =
    Multiset.sum
      (Multiset.map
        (fun (i_1 : ι) ↦
          HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
            ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
        s)
have e_a : (Multiset.map (α := R[X]) (HMul.hMul (f i))
      (Multiset.map
        (fun (i : ι) ↦
          HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
        s)).sum =
  Multiset.sum
    (Multiset.map
      (fun (i_1 : ι) ↦
        HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
          ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
      s)
Tactic: rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _,
    AddMonoidHom.coe_mulLeft]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
⊢ (Multiset.map (α := R[X]) (HMul.hMul (f i))
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s)).sum =
    Multiset.sum
      (Multiset.map
        (fun (i_1 : ι) ↦
          HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
            ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
        s)
have e_a : Eq.{u + 1} (α := R[X])
  (Multiset.sum
    (Multiset.map
      (fun (x : ι) ↦
        f i * HMul.hMul (β := R[X]) (Multiset.map f (s.erase x)).prod ((derivative : (a : R[X]) → R[X]) (f x) : R[X]))
      s))
  (Multiset.sum
    (Multiset.map
      (fun (i_1 : ι) ↦
        HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
          ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
      s))
Tactic: simp only [Function.comp_apply, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
⊢ Eq.{u + 1} (α := R[X])
    (Multiset.sum
      (Multiset.map
        (fun (x : ι) ↦
          f i * HMul.hMul (β := R[X]) (Multiset.map f (s.erase x)).prod ((derivative : (a : R[X]) → R[X]) (f x) : R[X]))
        s))
    (Multiset.sum
      (Multiset.map
        (fun (i_1 : ι) ↦
          HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase i_1)).prod
            ((derivative : (a : R[X]) → R[X]) (f i_1) : R[X]))
        s))
have e_a : ∀ (j : ι) (hj : j ∈ s),
  f i * HMul.hMul (β := R[X]) (Multiset.map f (s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
    HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
Tactic: refine congr_arg _ (Multiset.map_congr rfl fun j hj => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
j : ι
hj : j ∈ s
⊢ f i * HMul.hMul (β := R[X]) (Multiset.map f (s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
    HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
have e_a : HMul.hMul (β := R[X]) (Multiset.map f (i ::ₘ s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
  HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
Tactic: rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_cons]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
j : ι
hj : j ∈ s
⊢ HMul.hMul (β := R[X]) (Multiset.map f (i ::ₘ s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
    HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
have pos : ∀ (hij : i = j),
  HMul.hMul (β := R[X]) (Multiset.map f (i ::ₘ s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
    HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s_1 : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (Multiset.map f s).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (s.erase i)).prod ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          s) :
      R[X])
j : ι
hj : j ∈ s
pos :
  ∀ (hij : i = j),
    HMul.hMul (β := R[X]) (Multiset.map f (i ::ₘ s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
      HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
⊢ HMul.hMul (β := R[X]) (Multiset.map f (i ::ₘ s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
    HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
have neg : ∀ (hij : ¬i = j),
  HMul.hMul (β := R[X]) (Multiset.map f (i ::ₘ s.erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X]) =
    HMul.hMul (β := R[X]) (Multiset.map f ((i ::ₘ s).erase j)).prod ((derivative : (a : R[X]) → R[X]) (f j) : R[X])
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Ring R
c : R
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw : HSub.hSub (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
    ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
  1
Tactic: rw [derivative_sub, derivative_X, derivative_C, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Ring R
c : R
rw :
  HSub.hSub (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
    1
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw₁ : HSub.hSub (α := R[X]) (β := R[X]) (1 : R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) = 1
Tactic: rw [derivative_sub, derivative_X, derivative_C, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Ring R
c : R
rw :
  HSub.hSub (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
    1
rw₁ :
  HSub.hSub (α := R[X]) (β := R[X]) (1 : R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) = 1
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw₂ : HSub.hSub (α := R[X]) 1 0 = 1
Tactic: rw [derivative_sub, derivative_X, derivative_C, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Ring R
c : R
rw :
  HSub.hSub (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
    1
rw₁ :
  HSub.hSub (α := R[X]) (β := R[X]) (1 : R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) = 1
rw₂ : HSub.hSub (α := R[X]) 1 0 = 1
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X])
    (1 : R[X])
have rw₃ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [derivative_sub, derivative_X, derivative_C, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Ring R
n : ℤ
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) (↑n : R[X])) 0
have rw : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (↑n : R)) : R[X]) (0 : R[X])
Tactic: rw [← C_eq_intCast n]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Ring R
n : ℤ
k : ℕ
f : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[k] f
have zero : ∀ {f : R[X]},
  (⇑derivative : (a : R[X]) → R[X])^[0] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[0] f
Tactic: induction k generalizing f
Cleared hypotheses: k, f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Ring R
n : ℤ
k : ℕ
f : R[X]
zero :
  ∀ {f : R[X]},
    (⇑derivative : (a : R[X]) → R[X])^[0] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[0] f
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[k] f
have succ : ∀ (n_1 : ℕ),
  (∀ {f : R[X]},
      (⇑derivative : (a : R[X]) → R[X])^[n_1] ((↑n : R[X]) * f) =
        (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[n_1] f) →
    ∀ {f : R[X]},
      (⇑derivative : (a : R[X]) → R[X])^[n_1 + 1] ((↑n : R[X]) * f) =
        (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[n_1 + 1] f
Tactic: induction k generalizing f
Cleared hypotheses: k, f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    HPow.hPow (α := R[X]) (-1) k * ((⇑derivative : (a : R[X]) → R[X])^[k] p).comp (HSub.hSub (α := R[X]) 1 X)
have zero : ∀ (p : R[X]),
  (⇑derivative : (a : R[X]) → R[X])^[0] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    HPow.hPow (α := R[X]) (β := ℕ) (-1) 0 * ((⇑derivative : (a : R[X]) → R[X])^[0] p).comp (HSub.hSub (α := R[X]) 1 X)
Tactic: induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih (derivative p), derivative_comp, pow_succ]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
k : ℕ
zero :
  ∀ (p : R[X]),
    (⇑derivative : (a : R[X]) → R[X])^[0] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
      HPow.hPow (α := R[X]) (β := ℕ) (-1) 0 * ((⇑derivative : (a : R[X]) → R[X])^[0] p).comp (HSub.hSub (α := R[X]) 1 X)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    HPow.hPow (α := R[X]) (-1) k * ((⇑derivative : (a : R[X]) → R[X])^[k] p).comp (HSub.hSub (α := R[X]) 1 X)
have succ : ∀ (k : ℕ)
  (ih :
    ∀ (p : R[X]),
      (⇑derivative : (a : R[X]) → R[X])^[k] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
        HPow.hPow (α := R[X]) (-1) k * ((⇑derivative : (a : R[X]) → R[X])^[k] p).comp (HSub.hSub (α := R[X]) 1 X))
  (p : R[X]),
  (⇑derivative : (a : R[X]) → R[X])^[k + 1] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    HPow.hPow (α := R[X]) (-1) (k + 1) * ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).comp (HSub.hSub (α := R[X]) 1 X)
Tactic: induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih (derivative p), derivative_comp, pow_succ]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r
      ((derivative : (a : R[X]) → R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) S))) =
    Multiset.prod (Multiset.map (fun (a : R) ↦ r - a) (S.erase r))
have nth_rw : eval r
    ((derivative : (a : R[X]) → R[X])
      (Multiset.prod
        (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
          (r ::ₘ S.erase r)))) =
  Multiset.prod (Multiset.map (fun (a : R) ↦ r - a) (S.erase r))
Tactic: nth_rw 1 [← Multiset.cons_erase hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r
      ((derivative : (a : R[X]) → R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
            (r ::ₘ S.erase r)))) =
    Multiset.prod (Multiset.map (fun (a : R) ↦ r - a) (S.erase r))
have this : Eq (α := R)
  (((↑(evalRingHom r) : R[X] →* R) : (a : R[X]) → R)
      (Multiset.prod
        (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
          (S.erase r))) :
    R)
  (Multiset.prod
      (Multiset.map (α := R[X]) (⇑(↑(evalRingHom r) : R[X] →* R) : (a : R[X]) → R)
        (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
          (S.erase r))) :
    R)
Tactic: have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
c : R
m : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ m) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
have rw : HMul.hMul (β := R[X])
    ((C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1))
    ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
  (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
Tactic: rw [derivative_pow, derivative_X_sub_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
c : R
m : ℕ
rw :
  HMul.hMul (β := R[X])
      ((C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1))
      ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
⊢ (derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ m) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
have rw₁ : (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) * 1 =
  (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
Tactic: rw [derivative_pow, derivative_X_sub_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
c : R
m : ℕ
rw :
  HMul.hMul (β := R[X])
      ((C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1))
      ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
rw₁ :
  (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) * 1 =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
⊢ (derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ m) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
have rw₂ : (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) =
  (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
Tactic: rw [derivative_pow, derivative_X_sub_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
c : R
⊢ (derivative : (a : R[X]) → R[X])
      (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 2) =
    (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
have rw : HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]))
    ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
  (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
Tactic: rw [derivative_sq, derivative_X_sub_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
c : R
rw :
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]))
      ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 2) =
    (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
have rw₁ : (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) * 1 =
  (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
Tactic: rw [derivative_sq, derivative_X_sub_C, mul_one]