awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
simp :
  HMul.hMul (α := R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n]
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)))) :
            R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HSMul.hSMul (β := R[X]) (2 * (n + 1 + 1))
            ((⇑derivative : (a : R[X]) → R[X])^[n]
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p))) :
              R[X]) *
          X +
      HSMul.hSMul (β := R[X]) ((n + 1 + 1) * (n + 1))
        ((⇑derivative : (a : R[X]) → R[X])^[n] ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)) :
          R[X]) =
    HMul.hMul (α := R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n]
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)))) :
            R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        ((n + 1 + 1) * 2) •
          HMul.hMul (α := R[X]) (β := R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[n]
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p))) :
              R[X])
            X +
      HSMul.hSMul (β := R[X]) ((n + 1 + 1) * (n + 1))
        ((⇑derivative : (a : R[X]) → R[X])^[n] ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)) :
          R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1 + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))

Tactic:
simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]

Premises used: Nat.choose_two_right, nsmul_eq_mul, Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ HMul.hMul (α := R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n]
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)))) :
            R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HSMul.hSMul (β := R[X]) (2 * (n + 1 + 1))
            ((⇑derivative : (a : R[X]) → R[X])^[n]
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p))) :
              R[X]) *
          X +
      HSMul.hSMul (β := R[X]) ((n + 1 + 1) * (n + 1))
        ((⇑derivative : (a : R[X]) → R[X])^[n] ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)) :
          R[X]) =
    HMul.hMul (α := R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n]
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)))) :
            R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        ((n + 1 + 1) * 2) •
          HMul.hMul (α := R[X]) (β := R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[n]
                ((derivative : (a : R[X]) → R[X])
                  ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p))) :
              R[X])
            X +
      HSMul.hSMul (β := R[X]) ((n + 1 + 1) * (n + 1))
        ((⇑derivative : (a : R[X]) → R[X])^[n] ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)) :
          R[X])

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
h : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1 + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))

Tactic:
suffices ((n + 1 + 1) * (n + 1) / 2) * 2 = (n + 1 + 1) * (n + 1) by
    simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]
    ring
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
h : (n + 1) * (n + 1 + 1) / 2 * 2 = (n + 1) * (n + 1 + 1)
⊢ (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)

Tactic:
rw [mul_comm (n + 1 + 1)]

Premises used: HAdd.hAdd, mul_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (n + 1) * (n + 1 + 1) / 2 * 2 = (n + 1) * (n + 1 + 1)

Tactic:
Nat.div_mul_cancel (Nat.two_dvd_mul_add_one _)

Premises used: Nat.div_mul_cancel, Nat.two_dvd_mul_add_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (n + 1) * (n + 1 + 1) / 2 * 2 = (n + 1) * (n + 1 + 1)

Tactic:
exact Nat.div_mul_cancel (Nat.two_dvd_mul_add_one _)

Premises used: Nat.div_mul_cancel, Nat.two_dvd_mul_add_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
add :
  ∀ (p q_1 : R[X]),
    (derivative : (a : R[X]) → R[X]) (p.comp q) =
        HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
          (comp ((derivative : (a : R[X]) → R[X]) p) q) →
      (derivative : (a : R[X]) → R[X]) (q_1.comp q) =
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
            (comp ((derivative : (a : R[X]) → R[X]) q_1) q) →
        (derivative : (a : R[X]) → R[X]) ((p + q_1).comp q) =
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
            (comp ((derivative : (a : R[X]) → R[X]) (p + q_1)) q)
monomial :
  ∀ (n : ℕ) (a : R),
    (derivative : (a : R[X]) → R[X]) (comp ((Polynomial.monomial n : (a : R) → R[X]) a) q) =
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
        (comp ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial n : (a : R) → R[X]) a)) q)
⊢ (derivative : (a : R[X]) → R[X]) (p.comp q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) (comp ((derivative : (a : R[X]) → R[X]) p) q)

Tactic:
induction p using Polynomial.induction_on'
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
q p q_1 : R[X]
h :
  (derivative : (a : R[X]) → R[X]) (p.comp q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) (comp ((derivative : (a : R[X]) → R[X]) p) q)
h_1 :
  (derivative : (a : R[X]) → R[X]) (q_1.comp q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) (comp ((derivative : (a : R[X]) → R[X]) q_1) q)
⊢ (derivative : (a : R[X]) → R[X]) ((p + q_1).comp q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
      (comp ((derivative : (a : R[X]) → R[X]) (p + q_1)) q)

Tactic:
simp [*, mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
a : R
monomial :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (β := R[X]) ((↑n : R[X]) * q ^ (n - 1)) ((derivative : (a : R[X]) → R[X]) q : R[X])) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((↑n : R[X]) : R[X]) * q ^ (n - 1))
⊢ (derivative : (a : R[X]) → R[X]) (comp ((Polynomial.monomial n : (a : R) → R[X]) a) q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
      (comp ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial n : (a : R) → R[X]) a)) q)

Tactic:
simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C,
      zero_mul, C_eq_natCast, zero_add, map_mul]

Premises used: Polynomial.derivative_mul, Polynomial.derivative_monomial, MulZeroClass.zero_mul, Polynomial.C_eq_natCast, zero_add, map_mul, Polynomial.derivative_pow, Polynomial.derivative_C, Polynomial.monomial_comp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
a : R
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (β := R[X]) ((↑n : R[X]) * q ^ (n - 1)) ((derivative : (a : R[X]) → R[X]) q : R[X])) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((↑n : R[X]) : R[X]) * q ^ (n - 1))

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
r : R
rw :
  (derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ : 0 = HMul.hMul (β := R[X]) (eval₂ C q 0) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ : 0 = HMul.hMul (α := R[X]) (β := R[X]) (0 : R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₃ rw₄ : Eq.{u + 1} (α := R[X]) 0 0
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q ((C : (a : R) → R[X]) r)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])

Tactic:
rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]

Premises used: Polynomial.eval₂_zero, MulZeroClass.zero_mul, Polynomial.eval₂_C, Polynomial.derivative_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
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 0).prod : R[X])
    (Multiset.sum
        (Multiset.map
          (fun (i : ι) ↦
            HMul.hMul (β := R[X]) (Multiset.map f (Multiset.erase 0 i)).prod
              ((derivative : (a : R[X]) → R[X]) (f i) : R[X]))
          0) :
      R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s : Multiset ι
f : ι → R[X]
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])
⊢ 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])

Tactic:
refine Multiset.induction_on s (by simp) fun i s h => ?_
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
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)
⊢ 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:
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))]

Premises used: Polynomial.derivative, Polynomial.derivative_mul, Multiset.map_cons, Multiset.prod_cons, Multiset.erase_cons_head, mul_comm, Multiset.sum_cons, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
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)
⊢ 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:
congr
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
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)
⊢ 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:
rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _,
    AddMonoidHom.coe_mulLeft]

Premises used: AddMonoidHom.map_multiset_sum, AddMonoidHom.mulLeft, AddMonoidHom.coe_mulLeft
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
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))
⊢ (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:
simp only [Function.comp_apply, Multiset.map_map]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
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))

Tactic:
congr_arg _ (Multiset.map_congr rfl fun j hj => ?_)

Premises used: congr_arg, Multiset.map_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
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])
⊢ 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:
refine congr_arg _ (Multiset.map_congr rfl fun j hj => ?_)

Premises used: congr_arg, Multiset.map_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
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])
⊢ 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:
rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_cons]

Premises used: Multiset.map_cons, Multiset.prod_cons, mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
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])
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
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:
simp [hij, Multiset.cons_erase hj]

Premises used: Multiset.cons_erase
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
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:
simp [hij]