-- Mathlib/FieldTheory/Separable.lean
theorem exists_finset_of_splits (i : F →+* K) {f : F[X]} (sep : Separable f) (sp : Splits i f) :
    ∃ s : Finset K, f.map i = C (i f.leadingCoeff) * s.prod fun a : K => X - C a

Proof state:
case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : Splits i f
s : Multiset K
h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ ∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)

Tactic:
use s.toFinset

Result:
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : Splits i f
s : Multiset K
h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ map i f = C (i f.leadingCoeff) * ∏ a ∈ s.toFinset, (X - C a)

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

Tactic:
apply Separable.of_mul_right

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

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

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

Tactic:
apply nodup_of_separable_prod

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

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : Splits i f
⊢ ∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)

Tactic:
obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp

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

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : Splits i f
⊢ ∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)

Tactic:
classical
obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp
use s.toFinset
rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq]
apply nodup_of_separable_prod
apply Separable.of_mul_right
rw [← h]
exact sep.map

Result:
no goals

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

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

Tactic:
rw [← h]

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

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

Tactic:
exact sep.map

Result:
no goals

Proof state:
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : Splits i f
s : Multiset K
h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
⊢ map i f = C (i f.leadingCoeff) * ∏ a ∈ s.toFinset, (X - C a)

Tactic:
rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq]

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