-- Mathlib/Algebra/Polynomial/Splits.lean
theorem aeval_root_derivative_of_splits [Algebra K L] [DecidableEq L] {P : K[X]} (hmo : P.Monic)
    (hP : P.Splits (algebraMap K L)) {r : L} (hr : r ∈ P.aroots L) :
    aeval r (Polynomial.derivative P) =
    (((P.aroots L).erase r).map fun a => r - a).prod

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (derivative (map (algebraMap K L) P)) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Tactic:
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (derivative (Multiset.map (fun a => X - C a) (map (algebraMap K L) P).roots).prod) =
    (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (derivative (Multiset.map (fun a => X - C a) (map (algebraMap K L) P).roots).prod) =
    (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Tactic:
rw [eval_multiset_prod_X_sub_C_derivative hr]

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
hmo : P.Monic
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ P.aroots L
⊢ (aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Tactic:
replace hmo := hmo.map (algebraMap K L)

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
⊢ (aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
⊢ (aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Tactic:
replace hP := (splits_id_iff_splits (algebraMap K L)).2 hP

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ (aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Proof state:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ (aeval r) (derivative P) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod

Tactic:
rw [aeval_def, ← eval_map, ← derivative_map]

Result:
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
P : K[X]
r : L
hr : r ∈ P.aroots L
hmo : (map (algebraMap K L) P).Monic
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (derivative (map (algebraMap K L) P)) = (Multiset.map (fun a => r - a) ((P.aroots L).erase r)).prod