-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_exists_multiset {f : K[X]} {s : Multiset L}
    (hs : f.map i = C (i f.leadingCoeff) * (s.map fun a : L => X - C a).prod) : Splits i f :=
  letI := Classical.decEq K
  if hf0 : f = 0 then hf0.symm ▸ splits_zero i
  else
    Or.inr @fun p hp hdp => by
      rw [irreducible_iff_prime] at hp
      rw [hs, ← Multiset.prod_toList] at hdp
      obtain hd | hd := hp.2.2 _ _ hdp
      · refine (hp.2.1 <| isUnit_of_dvd_unit hd ?_).elim
        exact isUnit_C.2 ((leadingCoeff_ne_zero.2 hf0).isUnit.map i)
      · obtain ⟨q, hq, hd⟩ := hp.dvd_prod_iff.1 hd
        obtain ⟨a, _, rfl⟩ := Multiset.mem_map.1 (Multiset.mem_toList.1 hq)
        rw [degree_eq_degree_of_associated ((hp.dvd_prime_iff_associated <| prime_X_sub_C a).1 hd)]
        exact degree_X_sub_C a

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
⊢ p.degree = 1

Tactic:
obtain hd | hd := hp.2.2 _ _ hdp

Result:
case inl
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd : p ∣ C (i f.leadingCoeff)
⊢ p.degree = 1

case inr
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
⊢ p.degree = 1

Proof state:
case inr.intro.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd✝ : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
a : L
left✝ : a ∈ s
hq : X - C a ∈ (Multiset.map (fun a => X - C a) s).toList
hd : p ∣ X - C a
⊢ p.degree = 1

Tactic:
rw [degree_eq_degree_of_associated ((hp.dvd_prime_iff_associated <| prime_X_sub_C a).1 hd)]

Result:
case inr.intro.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd✝ : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
a : L
left✝ : a ∈ s
hq : X - C a ∈ (Multiset.map (fun a => X - C a) s).toList
hd : p ∣ X - C a
⊢ (X - C a).degree = 1

Proof state:
case inr.intro.intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd✝ : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
q : L[X]
hq : q ∈ (Multiset.map (fun a => X - C a) s).toList
hd : p ∣ q
⊢ p.degree = 1

Tactic:
obtain ⟨a, _, rfl⟩ := Multiset.mem_map.1 (Multiset.mem_toList.1 hq)

Result:
case inr.intro.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd✝ : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
a : L
left✝ : a ∈ s
hq : X - C a ∈ (Multiset.map (fun a => X - C a) s).toList
hd : p ∣ X - C a
⊢ p.degree = 1

Proof state:
case inr.intro.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd✝ : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
a : L
left✝ : a ∈ s
hq : X - C a ∈ (Multiset.map (fun a => X - C a) s).toList
hd : p ∣ X - C a
⊢ (X - C a).degree = 1

Tactic:
exact degree_X_sub_C a

Result:
no goals

Proof state:
case inl
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd : p ∣ C (i f.leadingCoeff)
⊢ IsUnit (C (i f.leadingCoeff))

Tactic:
exact isUnit_C.2 ((leadingCoeff_ne_zero.2 hf0).isUnit.map i)

Result:
no goals

Proof state:
case inl
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd : p ∣ C (i f.leadingCoeff)
⊢ p.degree = 1

Tactic:
refine (hp.2.1 <| isUnit_of_dvd_unit hd ?_).elim

Result:
case inl
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd : p ∣ C (i f.leadingCoeff)
⊢ IsUnit (C (i f.leadingCoeff))

Proof state:
case inr
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
⊢ p.degree = 1

Tactic:
obtain ⟨q, hq, hd⟩ := hp.dvd_prod_iff.1 hd

Result:
case inr.intro.intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
hd✝ : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod
q : L[X]
hq : q ∈ (Multiset.map (fun a => X - C a) s).toList
hd : p ∣ q
⊢ p.degree = 1

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ map i f
⊢ p.degree = 1

Tactic:
rw [hs, ← Multiset.prod_toList] at hdp

Result:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
this : DecidableEq K := Classical.decEq K
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod
⊢ p.degree = 1