case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ ∃ s, map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in s, (X - ↑C a)
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
⊢ ∃ s, map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in s, (X - ↑C a)
obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp
case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in Multiset.toFinset s, (X - ↑C a)
case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ ∃ s, map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in s, (X - ↑C a)
use s.toFinset
case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Multiset.Nodup s
case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in Multiset.toFinset s, (X - ↑C a)
rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq]
case intro.hs
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Multiset.Nodup s
apply nodup_of_separable_prod
case intro.hs.h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (?intro.hs.f * Multiset.prod (Multiset.map (fun a => X - ↑C a) s))

case intro.hs.f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ K[X]
case intro.hs
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
apply Separable.of_mul_right
case intro.hs.h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (map i f)
case intro.hs.h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (?intro.hs.f * Multiset.prod (Multiset.map (fun a => X - ↑C a) s))

case intro.hs.f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ K[X]
rw [← h]
no goals
case intro.hs.h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (map i f)
exact sep.map