R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (r ::ₘ Multiset.erase S r)))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) S))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
nth_rw 1 [← Multiset.cons_erase hr]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.erase S r))) =
    Multiset.prod (Multiset.map (↑(evalRingHom r)) (Multiset.map (fun a => X - ↑C a) (Multiset.erase S r)))
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (r ::ₘ Multiset.erase S r)))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (r ::ₘ Multiset.erase S r)))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))
no goals
R : Type u
S✝ : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
S : Multiset R
r : R
hr : r ∈ S
this :
  ↑(evalRingHom r) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (Multiset.erase S r))) =
    Multiset.prod (Multiset.map (↑(evalRingHom r)) (Multiset.map (fun a => X - ↑C a) (Multiset.erase S r)))
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (r ::ₘ Multiset.erase S r)))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase S r))
simpa using this