[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]


[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : comp p q = 0
⊢ natDegree (comp p q) ≤ natDegree p * natDegree q
[PROOFSTEP]
rw [h0, natDegree_zero]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : comp p q = 0
⊢ 0 ≤ natDegree p * natDegree q
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : ¬comp p q = 0
n : ℕ
hn : n ∈ support p
⊢ ↑(natDegree (↑C (coeff p n))) + n • ↑(natDegree q) = ↑(n * natDegree q)
[PROOFSTEP]
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h0 : ¬comp p q = 0
n : ℕ
hn : n ∈ support p
⊢ ↑n * ↑(natDegree q) = ↑(n * natDegree q)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : IsRoot p a
hlt : 0 ≥ degree p
⊢ False
[PROOFSTEP]
have := eq_C_of_degree_le_zero hlt
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : IsRoot p a
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
rw [IsRoot, this, eval_C] at h
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
simp only [h, RingHom.map_zero] at this
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
h : coeff p 0 = 0
hlt : 0 ≥ degree p
this : p = 0
⊢ False
[PROOFSTEP]
exact hp this
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ natDegree p ≤ n ↔ ∀ (N : ℕ), n < N → coeff p N = 0
[PROOFSTEP]
simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_withBot, WithBot.coe_lt_coe]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
⊢ natDegree (p + q) ≤ n ↔ natDegree p ≤ n
[PROOFSTEP]
refine' ⟨fun h => _, fun h => natDegree_add_le_of_degree_le h qn⟩
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
⊢ natDegree p ≤ n
[PROOFSTEP]
refine' natDegree_le_iff_coeff_eq_zero.mpr fun m hm => _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = 0
[PROOFSTEP]
convert natDegree_le_iff_coeff_eq_zero.mp h m hm using 1
[GOAL]
case h.e'_2
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
qn : natDegree q ≤ n
h : natDegree (p + q) ≤ n
m : ℕ
hm : n < m
⊢ coeff p m = coeff (p + q) m
[PROOFSTEP]
rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
pn : natDegree p ≤ n
⊢ natDegree (p + q) ≤ n ↔ natDegree q ≤ n
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : R[X]
pn : natDegree p ≤ n
⊢ natDegree (q + p) ≤ n ↔ natDegree q ≤ n
[PROOFSTEP]
exact natDegree_add_le_iff_left _ _ pn
[GOAL]
R : Type u
S : Type v
ι : Type w
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
⊢ natDegree (↑C a) + natDegree f = 0 + natDegree f
[PROOFSTEP]
rw [natDegree_C a]
[GOAL]
R : Type u
S : Type v
ι : Type w
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
a : R
⊢ natDegree f + natDegree (↑C a) = natDegree f + 0
[PROOFSTEP]
rw [natDegree_C a]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : ai * a = 1
⊢ natDegree p = natDegree (1 * p)
[PROOFSTEP]
nth_rw 1 [← one_mul p]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : ai * a = 1
⊢ natDegree (1 * p) = natDegree (↑C ai * (↑C a * p))
[PROOFSTEP]
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : a * ai = 1
⊢ natDegree p = natDegree (p * 1)
[PROOFSTEP]
nth_rw 1 [← mul_one p]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
ai : R
au : a * ai = 1
⊢ natDegree (p * 1) = natDegree (p * ↑C a * ↑C ai)
[PROOFSTEP]
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ natDegree (p * ↑C a) = natDegree p
[PROOFSTEP]
refine' eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ natDegree p ∈ support (p * ↑C a)
[PROOFSTEP]
refine' mem_support_iff.mpr _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : leadingCoeff p * a ≠ 0
⊢ coeff (p * ↑C a) (natDegree p) ≠ 0
[PROOFSTEP]
rwa [coeff_mul_C]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ natDegree (↑C a * p) = natDegree p
[PROOFSTEP]
refine' eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ natDegree p ∈ support (↑C a * p)
[PROOFSTEP]
refine' mem_support_iff.mpr _
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a * leadingCoeff p ≠ 0
⊢ coeff (↑C a * p) (natDegree p) ≠ 0
[PROOFSTEP]
rwa [coeff_C_mul]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f g : R[X]
⊢ coeff (f * g) (natDegree f + natDegree g) = coeff f (natDegree f) * coeff g (natDegree g)
[PROOFSTEP]
simp only [coeff_natDegree, coeff_mul_degree_add_degree]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
[PROOFSTEP]
rcases eq_or_lt_of_le pm with (rfl | hm)
[GOAL]
case inl
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
⊢ coeff (p * q) (natDegree p + n) = coeff p (natDegree p) * coeff q n
[PROOFSTEP]
rcases eq_or_lt_of_le qn with (rfl | hn)
[GOAL]
case inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
[PROOFSTEP]
rcases eq_or_lt_of_le qn with (rfl | hn)
[GOAL]
case inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ natDegree p
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (natDegree p + natDegree q) = coeff p (natDegree p) * coeff q (natDegree q)
[PROOFSTEP]
exact natDegree_add_coeff_mul _ _
[GOAL]
case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = coeff p (natDegree p) * coeff q n
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hn, mul_zero]
[GOAL]
case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = 0
[PROOFSTEP]
exact natDegree_lt_coeff_mul (add_lt_add_left hn _)
[GOAL]
case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = coeff p m * coeff q (natDegree q)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hm, zero_mul]
[GOAL]
case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = 0
[PROOFSTEP]
exact natDegree_lt_coeff_mul (add_lt_add_right hm _)
[GOAL]
case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hn, mul_zero]
[GOAL]
case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = 0
[PROOFSTEP]
exact natDegree_lt_coeff_mul (add_lt_add hm hn)
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
⊢ coeff (p ^ m) (m * n) = coeff p n ^ m
[PROOFSTEP]
induction' m with m hm
[GOAL]
case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
⊢ coeff (p ^ Nat.zero) (Nat.zero * n) = coeff p n ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (m * n) = coeff p n ^ m
⊢ coeff (p ^ Nat.succ m) (Nat.succ m * n) = coeff p n ^ Nat.succ m
[PROOFSTEP]
rw [pow_succ', pow_succ', ← hm, Nat.succ_mul, coeff_mul_of_natDegree_le _ pn]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (m * n) = coeff p n ^ m
⊢ natDegree (p ^ m) ≤ m * n
[PROOFSTEP]
refine' natDegree_pow_le.trans (le_trans _ (le_refl _))
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m✝ n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
m : ℕ
hm : coeff (p ^ m) (m * n) = coeff p n ^ m
⊢ m * natDegree p ≤ m * n
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left pn m.zero_le
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
o : ℕ
pn : natDegree p ≤ n
mno : m * n ≤ o
⊢ coeff (p ^ m) o = if o = m * n then coeff p n ^ m else 0
[PROOFSTEP]
rcases eq_or_ne o (m * n) with rfl | h
[GOAL]
case inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p ≤ n
mno : m * n ≤ m * n
⊢ coeff (p ^ m) (m * n) = if m * n = m * n then coeff p n ^ m else 0
[PROOFSTEP]
simpa only [ite_true] using coeff_pow_of_natDegree_le pn
[GOAL]
case inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
o : ℕ
pn : natDegree p ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ coeff (p ^ m) o = if o = m * n then coeff p n ^ m else 0
[PROOFSTEP]
simpa only [h, ite_false] using
  coeff_eq_zero_of_natDegree_lt $ lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p < n
⊢ coeff (p + q) n = coeff q n
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pn : natDegree p < n
⊢ coeff (q + p) n = coeff q n
[PROOFSTEP]
exact coeff_add_eq_left_of_lt pn
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum s f) = sup s fun i => degree (f i)
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH
[GOAL]
case empty
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
h : Set.Pairwise {i | i ∈ ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)
[PROOFSTEP]
simp
[GOAL]
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum (insert x s) f) = sup (insert x s) fun i => degree (f i)
[PROOFSTEP]
simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
[GOAL]
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
specialize IH (h.mono fun _ => by simp (config := { contextual := true }))
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
x✝ : S
⊢ x✝ ∈ {i | i ∈ s ∧ f i ≠ 0} → x✝ ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
[GOAL]
case insert.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) < degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
[GOAL]
case insert.inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hs)
[GOAL]
case insert.inr.inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
hx : ¬x ∈ ∅
h : Set.Pairwise {i | i ∈ insert x ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)
H : degree (f x) = degree (Finset.sum ∅ f)
⊢ degree (f x + Finset.sum ∅ fun x => f x) = degree (f x) ⊔ sup ∅ fun i => degree (f i)
[PROOFSTEP]
simp
[GOAL]
case insert.inr.inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
[GOAL]
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rw [IH, hy'] at H
[GOAL]
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
by_cases hx0 : f x = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
simp [hx0, IH]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
have hy0 : f y ≠ 0 := by
  contrapose! H
  simpa [H, degree_eq_bot] using hx0
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
⊢ f y ≠ 0
[PROOFSTEP]
contrapose! H
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
H : f y = 0
⊢ degree (f x) ≠ degree (f y)
[PROOFSTEP]
simpa [H, degree_eq_bot] using hx0
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
refine' absurd H (h _ _ fun H => hx _)
[GOAL]
case neg.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ x ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
[PROOFSTEP]
simp [hx0]
[GOAL]
case neg.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
[PROOFSTEP]
simp [hy, hy0]
[GOAL]
case neg.refine'_3
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H✝ : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s
[PROOFSTEP]
exact H.symm ▸ hy
[GOAL]
case insert.inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (Finset.sum s f) < degree (f x)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
[PROOFSTEP]
rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
by_cases H : ∃ x ∈ s, f x ≠ 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∃ x, x ∈ s ∧ f x ≠ 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
obtain ⟨x, hx, hx'⟩ := H
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
have hs : s.Nonempty := ⟨x, hx⟩
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
refine' natDegree_eq_of_degree_eq_some _
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ degree (Finset.sum s f) = ↑(sup s fun i => natDegree (f i))
[PROOFSTEP]
rw [degree_sum_eq_of_disjoint]
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ (sup s fun i => degree (f i)) = ↑(sup s fun i => natDegree (f i))
[PROOFSTEP]
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, Nat.cast_withBot, Finset.coe_sup' hs, ← Finset.sup'_eq_sup hs]
[GOAL]
case pos.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ (sup' s hs fun i => degree (f i)) = sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case pos.intro.intro.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ (sup' s hs fun i => degree (f i)) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
rw [Finset.sup'_le_iff]
[GOAL]
case pos.intro.intro.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ ∀ (b : S), b ∈ s → degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
intro b hb
[GOAL]
case pos.intro.intro.refine'_1
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
⊢ degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
by_cases hb' : f b = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
⊢ degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
simpa [hb'] using hs
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ degree (f b) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
rw [degree_eq_natDegree hb', Nat.cast_withBot]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ↑(natDegree (f b)) ≤ sup' s hs (WithBot.some ∘ fun i => natDegree (f i))
[PROOFSTEP]
exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ sup' s hs (WithBot.some ∘ fun i => natDegree (f i)) ≤ sup' s hs fun i => degree (f i)
[PROOFSTEP]
rw [Finset.sup'_le_iff]
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ ∀ (b : S), b ∈ s → (WithBot.some ∘ fun i => natDegree (f i)) b ≤ sup' s hs fun i => degree (f i)
[PROOFSTEP]
intro b hb
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
⊢ (WithBot.some ∘ fun i => natDegree (f i)) b ≤ sup' s hs fun i => degree (f i)
[PROOFSTEP]
simp only [Finset.le_sup'_iff, exists_prop, Function.comp_apply]
[GOAL]
case pos.intro.intro.refine'_2
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
⊢ ∃ b_1, b_1 ∈ s ∧ ↑(natDegree (f b)) ≤ degree (f b_1)
[PROOFSTEP]
by_cases hb' : f b = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ∃ b_1, b_1 ∈ s ∧ ↑(natDegree (f b)) ≤ degree (f b_1)
[PROOFSTEP]
refine' ⟨x, hx, _⟩
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ↑(natDegree (f b)) ≤ degree (f x)
[PROOFSTEP]
contrapose! hx'
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : f b = 0
hx' : degree (f x) < ↑(natDegree (f b))
⊢ f x = 0
[PROOFSTEP]
simpa [← Nat.cast_withBot, hb', degree_eq_bot] using hx'
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1, b_1 ∈ s ∧ ↑(natDegree (f b)) ≤ degree (f b_1)
[PROOFSTEP]
exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
[GOAL]
case pos.intro.intro.h
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : Finset.Nonempty s
⊢ Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
[PROOFSTEP]
exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ¬∃ x, x ∈ s ∧ f x ≠ 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
push_neg at H
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S), x ∈ s → f x = 0
⊢ natDegree (Finset.sum s f) = sup s fun i => natDegree (f i)
[PROOFSTEP]
rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S), x ∈ s → f x = 0
⊢ ∀ (s_1 : S), s_1 ∈ s → natDegree (f s_1) = ⊥
[PROOFSTEP]
intro x hx
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S), x ∈ s → f x = 0
x : S
hx : x ∈ s
⊢ natDegree (f x) = ⊥
[PROOFSTEP]
simp [H x hx]
[GOAL]
R : Type u
S : Type v
ι : Type w
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q r a : R[X]
⊢ max (natDegree (bit0 a)) (natDegree 1) ≤ natDegree a
[PROOFSTEP]
simp [natDegree_bit0]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
⊢ False
[PROOFSTEP]
have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
rw [A, eval₂_C] at hz
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = ↑C (coeff p 0)
⊢ False
[PROOFSTEP]
simp only [inj (p.coeff 0) hz, RingHom.map_zero] at A
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : ↑f (coeff p 0) = 0
inj : ∀ (x : R), ↑f x = 0 → x = 0
hlt : 0 ≥ natDegree p
A : p = 0
⊢ False
[PROOFSTEP]
exact hp A
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
⊢ ↑n < degree p ↔ n < natDegree p
[PROOFSTEP]
by_cases h : p = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < degree p ↔ n < natDegree p
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : ¬p = 0
⊢ ↑n < degree p ↔ n < natDegree p
[PROOFSTEP]
simp [degree_eq_natDegree h, Nat.cast_withBot, WithBot.coe_lt_coe]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
⊢ natDegree (p - q) = natDegree (q - p)
[PROOFSTEP]
rw [← natDegree_neg, neg_sub]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
qn : natDegree q ≤ n
⊢ natDegree (p - q) ≤ n ↔ natDegree p ≤ n
[PROOFSTEP]
rw [← natDegree_neg] at qn
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
qn : natDegree (-q) ≤ n
⊢ natDegree (p - q) ≤ n ↔ natDegree p ≤ n
[PROOFSTEP]
rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
pn : natDegree p ≤ n
⊢ natDegree (p - q) ≤ n ↔ natDegree q ≤ n
[PROOFSTEP]
rwa [natDegree_sub, natDegree_sub_le_iff_left]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
dg : natDegree q < n
⊢ coeff (p - q) n = coeff p n
[PROOFSTEP]
rw [← natDegree_neg] at dg
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
dg : natDegree (-q) < n
⊢ coeff (p - q) n = coeff p n
[PROOFSTEP]
rw [sub_eq_add_neg, coeff_add_eq_left_of_lt dg]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Ring R
p q : R[X]
df : natDegree p < n
⊢ coeff (p - q) n = -coeff q n
[PROOFSTEP]
rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ degree (p * ↑C a) = degree p
[PROOFSTEP]
rw [degree_mul, degree_C a0, add_zero]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ degree (↑C a * p) = degree p
[PROOFSTEP]
rw [degree_mul, degree_C a0, zero_add]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ natDegree (p * ↑C a) = natDegree p
[PROOFSTEP]
simp only [natDegree, degree_mul_C a0]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
a0 : a ≠ 0
⊢ natDegree (↑C a * p) = natDegree p
[PROOFSTEP]
simp only [natDegree, degree_C_mul a0]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
by_cases q0 : q.natDegree = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C, natDegree_C, mul_zero]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
by_cases p0 : p = 0
[GOAL]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
simp only [p0, zero_comp, natDegree_zero, zero_mul]
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
[PROOFSTEP]
refine' le_antisymm natDegree_comp_le (le_natDegree_of_ne_zero _)
[GOAL]
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ coeff (comp p q) (natDegree p * natDegree q) ≠ 0
[PROOFSTEP]
simp only [coeff_comp_degree_mul_degree q0, p0, mul_eq_zero, leadingCoeff_eq_zero, or_self_iff,
  ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), pow_ne_zero, Ne.def, not_false_iff]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
k : ℕ
⊢ natDegree ((comp p)^[k] q) = natDegree p ^ k * natDegree q
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ natDegree ((comp p)^[Nat.zero] q) = natDegree p ^ Nat.zero * natDegree q
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
k : ℕ
IH : natDegree ((comp p)^[k] q) = natDegree p ^ k * natDegree q
⊢ natDegree ((comp p)^[Nat.succ k] q) = natDegree p ^ Nat.succ k * natDegree q
[PROOFSTEP]
rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ, mul_assoc]
[GOAL]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : natDegree q ≠ 0
⊢ leadingCoeff (comp p q) = leadingCoeff p * leadingCoeff q ^ natDegree p
[PROOFSTEP]
rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]