[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
a : L
h : map i f = ↑C a
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
⊢ degree g✝ = 0
[PROOFSTEP]
have := congr_arg degree hp
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
a : L
h : map i f = ↑C a
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : degree (map i f) = degree (g✝ * p)
⊢ degree g✝ = 0
[PROOFSTEP]
rw [h, degree_C ha, degree_mul, @eq_comm (WithBot ℕ) 0, Nat.WithBot.add_eq_zero_iff] at this 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
a : L
h : map i f = ↑C a
ha : ¬a = 0
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : degree g✝ = 0 ∧ degree p = 0
⊢ degree g✝ = 0
[PROOFSTEP]
exact this.1
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree (map i f) = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
⊢ degree g✝ = 1
[PROOFSTEP]
have := congr_arg degree hp
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree (map i f) = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : degree (map i f) = degree (g✝ * p)
⊢ degree g✝ = 1
[PROOFSTEP]
simp [Nat.WithBot.add_eq_one_iff, hf, @eq_comm (WithBot ℕ) 1, mt isUnit_iff_degree_eq_zero.2 hg.1] at this 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree (map i f) = 1
g✝ : L[X]
hg : Irreducible g✝
x✝ : g✝ ∣ map i f
p : L[X]
hp : map i f = g✝ * p
this : degree g✝ = 1 ∧ degree p = 0
⊢ degree g✝ = 1
[PROOFSTEP]
tauto
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif : ¬degree (map i f) ≤ 0
⊢ Splits i f
[PROOFSTEP]
push_neg at hif 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif : 0 < degree (map i f)
⊢ Splits i f
[PROOFSTEP]
rw [← Order.succ_le_iff, ← WithBot.coe_zero, WithBot.succ_coe, Nat.succ_eq_succ] at hif 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : degree f ≤ 1
hif✝ : 0 < degree (map i f)
hif : ↑(Nat.succ 0) ≤ degree (map i f)
⊢ Splits i f
[PROOFSTEP]
exact splits_of_map_degree_eq_one i (le_antisymm ((degree_map_le i _).trans hf) hif)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g : K[X]
hf : Splits i f
hg : Splits i g
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
⊢ p ∣ map i f * map i g
[PROOFSTEP]
convert hpf
[GOAL]
case h.e'_4
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g : K[X]
hf : Splits i f
hg : Splits i g
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
⊢ map i f * map i g = map i (f * g)
[PROOFSTEP]
rw [Polynomial.map_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g : K[X]
hf✝ : Splits i f
hg : Splits i g
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
hf : map i f = 0
⊢ False
[PROOFSTEP]
simp [hf] at h 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g : K[X]
hf : Splits i f
hg✝ : Splits i g
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
hg : map i g = 0
⊢ False
[PROOFSTEP]
simp [hg] at h 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i (f * g✝)
[PROOFSTEP]
rw [Polynomial.map_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i f
⊢ g ∣ map i f * map i g✝
[PROOFSTEP]
exact hg.trans (dvd_mul_right _ _)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i (f * g✝)
[PROOFSTEP]
rw [Polynomial.map_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g✝ : K[X]
hfg : map i (f * g✝) ≠ 0
h : Splits i (f * g✝)
g : L[X]
hgi : Irreducible g
hg : g ∣ map i g✝
⊢ g ∣ map i f * map i g✝
[PROOFSTEP]
exact hg.trans (dvd_mul_left _ _)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
⊢ Splits j (map i f) ↔ Splits (RingHom.comp j i) f
[PROOFSTEP]
simp [Splits, Polynomial.map_map]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
[PROOFSTEP]
refine' Finset.induction_on t (fun _ => splits_one i) fun a t hat ih ht => _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : ∀ (j : ι), j ∈ insert a t → Splits i (s j)
⊢ Splits i (∏ x in insert a t, s x)
[PROOFSTEP]
rw [Finset.forall_mem_insert] at ht 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
⊢ Splits i (∏ x in insert a t, s x)
[PROOFSTEP]
rw [Finset.prod_insert hat]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → Splits i (s j)) → Splits i (∏ x in t, s x)
ht : Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
⊢ Splits i (s a * ∏ x in t, s x)
[PROOFSTEP]
exact splits_mul i ht.1 (ih ht.2)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : Splits i f
n : ℕ
⊢ Splits i (f ^ n)
[PROOFSTEP]
rw [← Finset.card_range n, ← Finset.prod_const]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : Splits i f
n : ℕ
⊢ Splits i (∏ _x in Finset.range n, f)
[PROOFSTEP]
exact splits_prod i fun j _ => hf
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
⊢ Splits (RingHom.id L) (map i f) ↔ Splits i f
[PROOFSTEP]
rw [splits_map_iff, RingHom.id_comp]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : degree (map i f) ≠ 0
hf0' : map i f = 0
⊢ ∃ x, eval₂ i x f = 0
[PROOFSTEP]
simp [eval₂_eq_eval_map, hf0']
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
f : K[X]
hs : Splits i✝ f
hf0 : degree (map i✝ f) ≠ 0
hf0' : ¬map i✝ f = 0
g : L[X]
hg : Irreducible g ∧ g ∣ map i✝ f
x : L
hx : IsRoot g x
i : L[X]
hi : map i✝ f = g * i
⊢ eval₂ i✝ x f = 0
[PROOFSTEP]
rw [← eval_map, hi, eval_mul, show _ = _ from hx, zero_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : natDegree (map i f) ≠ 0
x : L
hx : eval₂ i x f = 0
h : roots (map i f) = 0
⊢ False
[PROOFSTEP]
rw [← eval_map] at hx 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : natDegree (map i f) ≠ 0
x : L
hx : eval x (map i f) = 0
h : roots (map i f) = 0
⊢ False
[PROOFSTEP]
have : f.map i ≠ 0 := by intro; simp_all
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : natDegree (map i f) ≠ 0
x : L
hx : eval x (map i f) = 0
h : roots (map i f) = 0
⊢ map i f ≠ 0
[PROOFSTEP]
intro
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : natDegree (map i f) ≠ 0
x : L
hx : eval x (map i f) = 0
h : roots (map i f) = 0
a✝ : map i f = 0
⊢ False
[PROOFSTEP]
simp_all
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hs : Splits i f
hf0 : natDegree (map i f) ≠ 0
x : L
hx : eval x (map i f) = 0
h : roots (map i f) = 0
this : map i f ≠ 0
⊢ False
[PROOFSTEP]
cases h.subst ((mem_roots this).2 hx)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
[PROOFSTEP]
by_cases hp : p.map i = 0
[GOAL]
case pos
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : map i p = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
[PROOFSTEP]
rw [hp, natDegree_zero, roots_zero, Multiset.card_zero]
[GOAL]
case neg
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
[PROOFSTEP]
obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i)
[GOAL]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
q : L[X]
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
[PROOFSTEP]
rw [← splits_id_iff_splits, ← he] at hsplit 
[GOAL]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hp : ¬map i p = 0
q : L[X]
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
[PROOFSTEP]
rw [← he] at hp 
[GOAL]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
[PROOFSTEP]
have hq : q ≠ 0 := fun h => hp (by rw [h, mul_zero])
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
h : q = 0
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
[PROOFSTEP]
rw [h, mul_zero]
[GOAL]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
⊢ natDegree (map i p) = ↑Multiset.card (roots (map i p))
[PROOFSTEP]
rw [← hd, add_right_eq_self]
[GOAL]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
⊢ natDegree q = 0
[PROOFSTEP]
by_contra h
[GOAL]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
⊢ False
[PROOFSTEP]
have h' : (map (RingHom.id L) q).natDegree ≠ 0 := by simp [h]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
⊢ natDegree (map (RingHom.id L) q) ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ False
[PROOFSTEP]
have := roots_ne_zero_of_splits' (RingHom.id L) (splits_of_splits_mul' _ ?_ hsplit).2 h'
[GOAL]
case neg.intro.intro.intro.refine_2
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
this : roots (map (RingHom.id L) q) ≠ 0
⊢ False
[PROOFSTEP]
rw [map_id] at this 
[GOAL]
case neg.intro.intro.intro.refine_2
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
this : roots q ≠ 0
⊢ False
[PROOFSTEP]
exact this hr
[GOAL]
case neg.intro.intro.intro.refine_1
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ map (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q) ≠ 0
[PROOFSTEP]
rw [map_id]
[GOAL]
case neg.intro.intro.intro.refine_1
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = 0
hsplit : Splits (RingHom.id L) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q)
he : Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q = map i p
hd : ↑Multiset.card (roots (map i p)) + natDegree q = natDegree (map i p)
hr : roots q = 0
hq : q ≠ 0
h : ¬natDegree q = 0
h' : natDegree (map (RingHom.id L) q) ≠ 0
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) * q ≠ 0
[PROOFSTEP]
exact mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
p_ne_zero : map i p ≠ 0
hsplit : Splits i p
⊢ degree (map i p) = ↑(↑Multiset.card (roots (map i p)))
[PROOFSTEP]
simp [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots' hsplit]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
⊢ Splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, Irreducible g → g ∣ map i f → degree g = 1
[PROOFSTEP]
rw [Splits, map_eq_zero]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f g : K[X]
hf0 : f ≠ 0
hf : Splits i f
hgf : g ∣ f
⊢ Splits i g
[PROOFSTEP]
obtain ⟨f, rfl⟩ := hgf
[GOAL]
case intro
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
g f : K[X]
hf0 : g * f ≠ 0
hf : Splits i (g * f)
⊢ Splits i g
[PROOFSTEP]
exact (splits_of_splits_mul i hf0 hf).1
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
[PROOFSTEP]
refine'
  Finset.induction_on t (fun _ => ⟨fun _ _ h => by simp only [Finset.not_mem_empty] at h , fun _ => splits_one i⟩)
    fun a t hat ih ht => _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
x✝² : ∀ (j : ι), j ∈ ∅ → s j ≠ 0
x✝¹ : Splits i (∏ x in ∅, s x)
x✝ : ι
h : x✝ ∈ ∅
⊢ Splits i (s x✝)
[PROOFSTEP]
simp only [Finset.not_mem_empty] at h 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
ht : ∀ (j : ι), j ∈ insert a t → s j ≠ 0
⊢ Splits i (∏ x in insert a t, s x) ↔ ∀ (j : ι), j ∈ insert a t → Splits i (s j)
[PROOFSTEP]
rw [Finset.forall_mem_insert] at ht ⊢
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : ¬a ∈ t
ih : (∀ (j : ι), j ∈ t → s j ≠ 0) → (Splits i (∏ x in t, s x) ↔ ∀ (j : ι), j ∈ t → Splits i (s j))
ht : s a ≠ 0 ∧ ∀ (x : ι), x ∈ t → s x ≠ 0
⊢ Splits i (∏ x in insert a t, s x) ↔ Splits i (s a) ∧ ∀ (x : ι), x ∈ t → Splits i (s x)
[PROOFSTEP]
rw [Finset.prod_insert hat, splits_mul_iff i ht.1 (Finset.prod_ne_zero_iff.2 ht.2), ih ht.2]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : Splits (RingHom.id K) p
⊢ degree p = 1
[PROOFSTEP]
rcases hp_splits with ⟨⟩ | hp_splits
[GOAL]
case inl
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ degree p = 1
[PROOFSTEP]
exfalso
[GOAL]
case inl.h
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ False
[PROOFSTEP]
simp_all
[GOAL]
case inr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → degree g = 1
⊢ degree p = 1
[PROOFSTEP]
apply hp_splits hp
[GOAL]
case inr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → degree g = 1
⊢ p ∣ map (RingHom.id K) p
[PROOFSTEP]
simp
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
p_ne_zero : p ≠ 0
hsplit : Splits i p
⊢ degree p = ↑(↑Multiset.card (roots (map i p)))
[PROOFSTEP]
rw [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots hsplit]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : Splits (RingHom.id K) f
⊢ ↑Multiset.card (roots f) = natDegree f
[PROOFSTEP]
convert (natDegree_eq_card_roots hf).symm
[GOAL]
case h.e'_2.h.e'_6.h.e'_4
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
hf : Splits (RingHom.id K) f
⊢ f = map (RingHom.id K) f
[PROOFSTEP]
rw [map_id]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ ↑f '' rootSet p K = rootSet p L
[PROOFSTEP]
classical rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom, ←
  roots_map _ ((splits_id_iff_splits (algebraMap F K)).mpr h), map_map, f.comp_algebraMap, ← rootSet]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ ↑f '' rootSet p K = rootSet p L
[PROOFSTEP]
rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom, ←
  roots_map _ ((splits_id_iff_splits (algebraMap F K)).mpr h), map_map, f.comp_algebraMap, ← rootSet]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ Algebra.adjoin F (rootSet p L) = AlgHom.range f ↔ Algebra.adjoin F (rootSet p K) = ⊤
[PROOFSTEP]
rw [← image_rootSet h f, Algebra.adjoin_image, ← Algebra.map_top]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
p : F[X]
h : Splits (algebraMap F K) p
f : K →ₐ[F] L
⊢ Subalgebra.map f (Algebra.adjoin F (rootSet p K)) = Subalgebra.map f ⊤ ↔ Algebra.adjoin F (rootSet p K) = ⊤
[PROOFSTEP]
exact (Subalgebra.map_injective f.toRingHom.injective).eq_iff
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ map i p = ↑C (↑i (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p)))
[PROOFSTEP]
rw [← leadingCoeff_map]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ map i p = ↑C (leadingCoeff (map i p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p)))
[PROOFSTEP]
symm
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ ↑C (leadingCoeff (map i p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) = map i p
[PROOFSTEP]
apply C_leadingCoeff_mul_prod_multiset_X_sub_C
[GOAL]
case hroots
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ ↑Multiset.card (roots (map i p)) = natDegree (map i p)
[PROOFSTEP]
rw [natDegree_map]
[GOAL]
case hroots
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ ↑Multiset.card (roots (map i p)) = natDegree p
[PROOFSTEP]
exact (natDegree_eq_card_roots hsplit).symm
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hsplit : Splits (RingHom.id K) p
⊢ p = ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
[PROOFSTEP]
simpa using eq_prod_roots_of_splits hsplit
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
m : Monic p
hsplit : Splits (RingHom.id K) p
⊢ p = Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
[PROOFSTEP]
convert eq_prod_roots_of_splits_id hsplit
[GOAL]
case h.e'_3
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
m : Monic p
hsplit : Splits (RingHom.id K) p
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)) =
    ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
[PROOFSTEP]
simp [m]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ h = ↑C (leadingCoeff h) * (X - ↑C x)
[PROOFSTEP]
apply Polynomial.map_injective _ i.injective
[GOAL]
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ map i h = map i (↑C (leadingCoeff h) * (X - ↑C x))
[PROOFSTEP]
rw [eq_prod_roots_of_splits h_splits, h_roots]
[GOAL]
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ ↑C (↑i (leadingCoeff h)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) {↑i x}) =
    map i (↑C (leadingCoeff h) * (X - ↑C x))
[PROOFSTEP]
simp
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
⊢ f ∈ lifts (algebraMap R K)
[PROOFSTEP]
rw [eq_prod_roots_of_monic_of_splits_id hm hs, lifts_iff_liftsRing]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots f)) ∈ liftsRing (algebraMap R K)
[PROOFSTEP]
refine' Subring.multiset_prod_mem _ _ fun P hP => _
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
P : K[X]
hP : P ∈ Multiset.map (fun a => X - ↑C a) (roots f)
⊢ P ∈ liftsRing (algebraMap R K)
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := Multiset.mem_map.1 hP
[GOAL]
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
i : K →+* L
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R K
f : K[X]
hs : Splits (RingHom.id K) f
hm : Monic f
hr : ∀ (a : K), a ∈ roots f → a ∈ RingHom.range (algebraMap R K)
b : K
hb : b ∈ roots f
hP : X - ↑C b ∈ Multiset.map (fun a => X - ↑C a) (roots f)
⊢ X - ↑C b ∈ liftsRing (algebraMap R K)
[PROOFSTEP]
exact Subring.sub_mem _ (X_mem_lifts _) (C'_mem_lifts (hr _ hb))
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Irreducible p
hdp : p ∣ map i f
⊢ degree p = 1
[PROOFSTEP]
rw [irreducible_iff_prime] at hp 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ map i f
⊢ degree p = 1
[PROOFSTEP]
rw [hs, ← Multiset.prod_toList] at hdp 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ ↑C (↑i (leadingCoeff f)) * List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
⊢ degree p = 1
[PROOFSTEP]
obtain hd | hd := hp.2.2 _ _ hdp
[GOAL]
case inl
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ ↑C (↑i (leadingCoeff f)) * List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
hd : p ∣ ↑C (↑i (leadingCoeff f))
⊢ degree p = 1
[PROOFSTEP]
refine' (hp.2.1 <| isUnit_of_dvd_unit hd _).elim
[GOAL]
case inl
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ ↑C (↑i (leadingCoeff f)) * List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
hd : p ∣ ↑C (↑i (leadingCoeff f))
⊢ IsUnit (↑C (↑i (leadingCoeff f)))
[PROOFSTEP]
exact isUnit_C.2 ((leadingCoeff_ne_zero.2 hf0).isUnit.map i)
[GOAL]
case inr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ ↑C (↑i (leadingCoeff f)) * List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
hd : p ∣ List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
⊢ degree p = 1
[PROOFSTEP]
obtain ⟨q, hq, hd⟩ := hp.dvd_prod_iff.1 hd
[GOAL]
case inr.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ ↑C (↑i (leadingCoeff f)) * List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
hd✝ : p ∣ List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
q : L[X]
hq : q ∈ Multiset.toList (Multiset.map (fun a => X - ↑C a) s)
hd : p ∣ q
⊢ degree p = 1
[PROOFSTEP]
obtain ⟨a, _, rfl⟩ := Multiset.mem_map.1 (Multiset.mem_toList.1 hq)
[GOAL]
case inr.intro.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ ↑C (↑i (leadingCoeff f)) * List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
hd✝ : p ∣ List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
a : L
left✝ : a ∈ s
hq : X - ↑C a ∈ Multiset.toList (Multiset.map (fun a => X - ↑C a) s)
hd : p ∣ X - ↑C a
⊢ degree p = 1
[PROOFSTEP]
rw [degree_eq_degree_of_associated ((hp.dvd_prime_iff_associated <| prime_X_sub_C a).1 hd)]
[GOAL]
case inr.intro.intro.intro.intro
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f : K[X]
s : Multiset L
hs : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
hf0 : ¬f = 0
p : L[X]
hp : Prime p
hdp : p ∣ ↑C (↑i (leadingCoeff f)) * List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
hd✝ : p ∣ List.prod (Multiset.toList (Multiset.map (fun a => X - ↑C a) s))
a : L
left✝ : a ∈ s
hq : X - ↑C a ∈ Multiset.toList (Multiset.map (fun a => X - ↑C a) s)
hd : p ∣ X - ↑C a
⊢ degree (X - ↑C a) = 1
[PROOFSTEP]
exact degree_X_sub_C a
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f x✝¹ : K[X]
hu : IsUnit x✝¹
x✝ : Splits (RingHom.id K) x✝¹
⊢ 0 ≤ 1
[PROOFSTEP]
decide
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
f a p : K[X]
ha0 : a ≠ 0
hp : Prime p
ih : Splits (RingHom.id K) a → Splits i a
hfi : Splits (RingHom.id K) (p * a)
⊢ p ∣ map (RingHom.id K) p
[PROOFSTEP]
rw [map_id]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits i f
⊢ Splits (RingHom.comp j i) f
[PROOFSTEP]
rw [← splits_map_iff]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits i f
⊢ Splits j (map i f)
[PROOFSTEP]
rw [← RingHom.id_comp i, ← splits_map_iff i] at h 
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
j : L →+* F
f : K[X]
h : Splits (RingHom.id L) (map i f)
⊢ Splits j (map i f)
[PROOFSTEP]
exact splits_of_splits_id _ h
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
⊢ Splits (RingHom.id K) p ↔ ↑Multiset.card (roots p) = natDegree p
[PROOFSTEP]
constructor
[GOAL]
case mp
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
⊢ Splits (RingHom.id K) p → ↑Multiset.card (roots p) = natDegree p
[PROOFSTEP]
intro H
[GOAL]
case mp
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
H : Splits (RingHom.id K) p
⊢ ↑Multiset.card (roots p) = natDegree p
[PROOFSTEP]
rw [natDegree_eq_card_roots H, map_id]
[GOAL]
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
⊢ ↑Multiset.card (roots p) = natDegree p → Splits (RingHom.id K) p
[PROOFSTEP]
intro hroots
[GOAL]
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ Splits (RingHom.id K) p
[PROOFSTEP]
rw [splits_iff_exists_multiset (RingHom.id K)]
[GOAL]
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ ∃ s, map (RingHom.id K) p = ↑C (↑(RingHom.id K) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
[PROOFSTEP]
use p.roots
[GOAL]
case h
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ map (RingHom.id K) p =
    ↑C (↑(RingHom.id K) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
[PROOFSTEP]
simp only [RingHom.id_apply, map_id]
[GOAL]
case h
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ p = ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots p))
[PROOFSTEP]
exact (C_leadingCoeff_mul_prod_multiset_X_sub_C hroots).symm
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
hmo : Monic P
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ roots (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
[PROOFSTEP]
replace hmo := hmo.map (algebraMap K L)
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
[PROOFSTEP]
replace hP := (splits_id_iff_splits (algebraMap K L)).2 hP
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
[PROOFSTEP]
rw [aeval_def, ← eval_map, ← derivative_map]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (↑derivative (map (algebraMap K L) P)) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
[PROOFSTEP]
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map (algebraMap K L) P))))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
[PROOFSTEP]
rw [eval_multiset_prod_X_sub_C_derivative hr]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ coeff P 0 = (-1) ^ natDegree P * Multiset.prod (roots P)
[PROOFSTEP]
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ coeff (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots P))) 0 = (-1) ^ natDegree P * Multiset.prod (roots P)
[PROOFSTEP]
rw [coeff_zero_eq_eval_zero, eval_multiset_prod, Multiset.map_map]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ Multiset.prod (Multiset.map (eval 0 ∘ fun a => X - ↑C a) (roots P)) = (-1) ^ natDegree P * Multiset.prod (roots P)
[PROOFSTEP]
simp_rw [Function.comp_apply, eval_sub, eval_X, zero_sub, eval_C]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ Multiset.prod (Multiset.map (fun x => -x) (roots P)) = (-1) ^ natDegree P * Multiset.prod (roots P)
[PROOFSTEP]
conv_lhs =>
  congr
  congr
  ext
  rw [neg_eq_neg_one_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
| Multiset.prod (Multiset.map (fun x => -x) (roots P))
[PROOFSTEP]
  congr
  congr
  ext
  rw [neg_eq_neg_one_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
| Multiset.prod (Multiset.map (fun x => -x) (roots P))
[PROOFSTEP]
  congr
  congr
  ext
  rw [neg_eq_neg_one_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
| Multiset.prod (Multiset.map (fun x => -x) (roots P))
[PROOFSTEP]
congr
[GOAL]
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
| Multiset.map (fun x => -x) (roots P)
[PROOFSTEP]
congr
[GOAL]
case a.f
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
| fun x => -x
case a.s
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
| roots P
[PROOFSTEP]
ext
[GOAL]
case a.f.h
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
x✝ : K
| -x✝
case a.s
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
| roots P
[PROOFSTEP]
rw [neg_eq_neg_one_mul]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ Multiset.prod (Multiset.map (fun x => -1 * x) (roots P)) = (-1) ^ natDegree P * Multiset.prod (roots P)
[PROOFSTEP]
simp only [splits_iff_card_roots.1 hP, neg_mul, one_mul, Multiset.prod_map_neg]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ nextCoeff P = -Multiset.sum (roots P)
[PROOFSTEP]
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ nextCoeff (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots P))) = -Multiset.sum (roots P)
[PROOFSTEP]
rw [Monic.nextCoeff_multiset_prod _ _ fun a ha => _]
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ Multiset.sum (Multiset.map (fun i => nextCoeff (X - ↑C i)) (roots P)) = -Multiset.sum (roots P)
[PROOFSTEP]
simp_rw [nextCoeff_X_sub_C, Multiset.sum_map_neg']
[GOAL]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ ∀ (a : K), a ∈ roots P → Monic (X - ↑C a)
[PROOFSTEP]
simp only [monic_X_sub_C, implies_true]
