[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial R
⊢ ¬Separable 0
[PROOFSTEP]
rintro ⟨x, y, h⟩
[GOAL]
case intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial R
x y : R[X]
h : x * 0 + y * ↑derivative 0 = 1
⊢ False
[PROOFSTEP]
simp only [derivative_zero, mul_zero, add_zero, zero_ne_one] at h
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Subsingleton R
f : R[X]
⊢ Separable f
[PROOFSTEP]
simp [Separable, IsCoprime]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
a : R
⊢ Separable (X + ↑C a)
[PROOFSTEP]
rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
a : R
⊢ IsCoprime (X + ↑C a) 1
[PROOFSTEP]
exact isCoprime_one_right
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
⊢ Separable X
[PROOFSTEP]
rw [separable_def, derivative_X]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
⊢ IsCoprime X 1
[PROOFSTEP]
exact isCoprime_one_right
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
r : R
⊢ Separable (↑C r) ↔ IsUnit r
[PROOFSTEP]
rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
⊢ Separable f
[PROOFSTEP]
have := h.of_mul_left_left
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative (f * g))
⊢ Separable f
[PROOFSTEP]
rw [derivative_mul] at this
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative f * g + f * ↑derivative g)
⊢ Separable f
[PROOFSTEP]
exact IsCoprime.of_mul_right_left (IsCoprime.of_add_mul_left_right this)
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
⊢ Separable g
[PROOFSTEP]
rw [mul_comm] at h
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (g * f)
⊢ Separable g
[PROOFSTEP]
exact h.of_mul_left
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
hf : Separable f
hfg : g ∣ f
⊢ Separable g
[PROOFSTEP]
rcases hfg with ⟨f', rfl⟩
[GOAL]
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
g f' : R[X]
hf : Separable (g * f')
⊢ Separable g
[PROOFSTEP]
exact Separable.of_mul_left hf
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
⊢ IsCoprime f g
[PROOFSTEP]
have := h.of_mul_left_left
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative (f * g))
⊢ IsCoprime f g
[PROOFSTEP]
rw [derivative_mul] at this
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f g : R[X]
h : Separable (f * g)
this : IsCoprime f (↑derivative f * g + f * ↑derivative g)
⊢ IsCoprime f g
[PROOFSTEP]
exact IsCoprime.of_mul_right_right (IsCoprime.of_add_mul_left_right this)
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R[X]
n : ℕ
h : Separable (f ^ (n + 2))
⊢ IsUnit f ∨ Separable f ∧ n + 2 = 1 ∨ n + 2 = 0
[PROOFSTEP]
rw [pow_succ, pow_succ] at h
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
f : R[X]
n : ℕ
h : Separable (f * (f * f ^ n))
⊢ IsUnit f ∨ Separable f ∧ n + 2 = 1 ∨ n + 2 = 0
[PROOFSTEP]
exact Or.inl (isCoprime_self.1 h.isCoprime.of_mul_right_left)
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : Separable p
f : R →+* S
a b : R[X]
H : a * p + b * ↑derivative p = 1
⊢ Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * ↑derivative (Polynomial.map f p) = 1
[PROOFSTEP]
rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H, Polynomial.map_one]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hp : Separable p
hq : q * q ∣ p
⊢ IsUnit q
[PROOFSTEP]
obtain ⟨p, rfl⟩ := hq
[GOAL]
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsUnit q
[PROOFSTEP]
apply isCoprime_self.mp
[GOAL]
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime q q
[PROOFSTEP]
have : IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p)) :=
  by
  simp only [← mul_assoc, mul_add]
  dsimp only [Separable] at hp
  convert hp using 1
  rw [derivative_mul, derivative_mul]
  ring
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime (q * (q * p)) (q * (↑derivative q * p + ↑derivative q * p + q * ↑derivative p))
[PROOFSTEP]
simp only [← mul_assoc, mul_add]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
⊢ IsCoprime (q * q * p) (q * ↑derivative q * p + q * ↑derivative q * p + q * q * ↑derivative p)
[PROOFSTEP]
dsimp only [Separable] at hp
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : IsCoprime (q * q * p) (↑derivative (q * q * p))
⊢ IsCoprime (q * q * p) (q * ↑derivative q * p + q * ↑derivative q * p + q * q * ↑derivative p)
[PROOFSTEP]
convert hp using 1
[GOAL]
case h.e'_4
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : IsCoprime (q * q * p) (↑derivative (q * q * p))
⊢ q * ↑derivative q * p + q * ↑derivative q * p + q * q * ↑derivative p = ↑derivative (q * q * p)
[PROOFSTEP]
rw [derivative_mul, derivative_mul]
[GOAL]
case h.e'_4
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : IsCoprime (q * q * p) (↑derivative (q * q * p))
⊢ q * ↑derivative q * p + q * ↑derivative q * p + q * q * ↑derivative p =
    (↑derivative q * q + q * ↑derivative q) * p + q * q * ↑derivative p
[PROOFSTEP]
ring
[GOAL]
case intro
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
q p : R[X]
hp : Separable (q * q * p)
this : IsCoprime (q * (q * p)) (q * (↑derivative q * p + ↑derivative q * p + q * ↑derivative p))
⊢ IsCoprime q q
[PROOFSTEP]
exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hq : ¬IsUnit q
hsep : Separable p
⊢ multiplicity q p ≤ 1
[PROOFSTEP]
contrapose! hq
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ IsUnit q
[PROOFSTEP]
apply isUnit_of_self_mul_dvd_separable hsep
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ q * q ∣ p
[PROOFSTEP]
rw [← sq]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ q ^ 2 ∣ p
[PROOFSTEP]
apply multiplicity.pow_dvd_of_le_multiplicity
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ ↑2 ≤ multiplicity q p
[PROOFSTEP]
have h : ⟨Part.Dom 1 ∧ Part.Dom 1, fun _ ↦ 2⟩ ≤ multiplicity q p := PartENat.add_one_le_of_lt hq
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
h : { Dom := 1.Dom ∧ 1.Dom, get := fun x => 2 } ≤ multiplicity q p
⊢ ↑2 ≤ multiplicity q p
[PROOFSTEP]
rw [and_self] at h
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
h : { Dom := 1.Dom, get := fun x => 2 } ≤ multiplicity q p
⊢ ↑2 ≤ multiplicity q p
[PROOFSTEP]
exact h
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q : ℕ
p : R[X]
hsep : Separable p
⊢ Squarefree p
[PROOFSTEP]
rw [multiplicity.squarefree_iff_multiplicity_le_one p]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q : ℕ
p : R[X]
hsep : Separable p
⊢ ∀ (x : R[X]), multiplicity x p ≤ 1 ∨ IsUnit x
[PROOFSTEP]
exact fun f => or_iff_not_imp_right.mpr fun hunit => multiplicity_le_one_of_separable hunit hsep
[GOAL]
R : Type u
inst✝ : CommRing R
x : R
⊢ Separable (X - ↑C x)
[PROOFSTEP]
simpa only [sub_eq_add_neg, C_neg] using separable_X_add_C (-x)
[GOAL]
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : Separable f
hg : Separable g
h : IsCoprime f g
⊢ Separable (f * g)
[PROOFSTEP]
rw [separable_def, derivative_mul]
[GOAL]
R : Type u
inst✝ : CommRing R
f g : R[X]
hf : Separable f
hg : Separable g
h : IsCoprime f g
⊢ IsCoprime (f * g) (↑derivative f * g + f * ↑derivative g)
[PROOFSTEP]
exact ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)
[GOAL]
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h1 : ∀ (x : ι), x ∈ insert a s → ∀ (y : ι), y ∈ insert a s → x ≠ y → IsCoprime (f x) (f y)
h2 : ∀ (x : ι), x ∈ insert a s → Separable (f x)
⊢ Separable (∏ x in insert a s, f x)
[PROOFSTEP]
simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2
[GOAL]
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h2 : Separable (f a) ∧ ∀ (x : ι), x ∈ s → Separable (f x)
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ (x : ι), x ∈ s → a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι), x ∈ s → x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ Separable (∏ x in insert a s, f x)
[PROOFSTEP]
rw [prod_insert has]
[GOAL]
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : ¬a ∈ s
ih :
  (∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) →
    (∀ (x : ι), x ∈ s → Separable (f x)) → Separable (∏ x in s, f x)
h2 : Separable (f a) ∧ ∀ (x : ι), x ∈ s → Separable (f x)
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ (x : ι), x ∈ s → a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι), x ∈ s → x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι), x ∈ s → ∀ (x_2 : ι), x_2 ∈ s → x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ Separable (f a * ∏ x in s, f x)
[PROOFSTEP]
exact
  h2.1.mul (ih h1.2.2 h2.2) (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable (∏ i in s, (X - ↑C (f i)))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
⊢ x = y
[PROOFSTEP]
by_contra hxy
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable (∏ i in s, (X - ↑C (f i)))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
[PROOFSTEP]
rw [← insert_erase hx, prod_insert (not_mem_erase _ _), ← insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy),
  prod_insert (not_mem_erase _ _), ← mul_assoc, hfxy, ← sq] at hfs
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs : Separable ((X - ↑C (f y)) ^ 2 * ∏ x in Finset.erase (Finset.erase s x) y, (X - ↑C (f x)))
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
[PROOFSTEP]
cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
⊢ Multiset.Nodup s
[PROOFSTEP]
rw [Multiset.nodup_iff_ne_cons_cons]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
⊢ ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
[PROOFSTEP]
rintro a t rfl
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t)))
⊢ False
[PROOFSTEP]
refine' not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs _)
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t)))
⊢ (X - ↑C a) * (X - ↑C a) ∣ Multiset.prod (Multiset.map (fun a => X - ↑C a) (a ::ₘ a ::ₘ t))
[PROOFSTEP]
simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)
[GOAL]
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
⊢ Separable (X ^ n - ↑C ↑u)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
⊢ Separable (X ^ n - ↑C ↑u)
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hpos)
[GOAL]
case inl
R : Type u
inst✝ : CommRing R
u : Rˣ
✝ : Nontrivial R
hn : IsUnit ↑0
⊢ Separable (X ^ 0 - ↑C ↑u)
[PROOFSTEP]
simp at hn
[GOAL]
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
⊢ Separable (X ^ n - ↑C ↑u)
[PROOFSTEP]
apply (separable_def' (X ^ n - C (u : R))).2
[GOAL]
case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
⊢ ∃ a b, a * (X ^ n - ↑C ↑u) + b * ↑derivative (X ^ n - ↑C ↑u) = 1
[PROOFSTEP]
obtain ⟨n', hn'⟩ := hn.exists_left_inv
[GOAL]
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ ∃ a b, a * (X ^ n - ↑C ↑u) + b * ↑derivative (X ^ n - ↑C ↑u) = 1
[PROOFSTEP]
refine' ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, _⟩
[GOAL]
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -↑C ↑u⁻¹ * (X ^ n - ↑C ↑u) + ↑C ↑u⁻¹ * ↑C n' * X * ↑derivative (X ^ n - ↑C ↑u) = 1
[PROOFSTEP]
rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]
[GOAL]
case inr.intro
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -↑C ↑u⁻¹ * (X ^ n - ↑C ↑u) + ↑C ↑u⁻¹ * ↑C n' * X * (↑C ↑n * X ^ (n - 1)) = 1
[PROOFSTEP]
calc
  -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
      C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) :=
    by
    simp only [C.map_mul, C_eq_nat_cast]
    ring
  _ = 1 := by
    simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ, Nat.sub_add_cancel (show 1 ≤ n from hpos),
      sub_add_cancel]
[GOAL]
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -↑C ↑u⁻¹ * (X ^ n - ↑C ↑u) + ↑C ↑u⁻¹ * ↑C n' * X * (↑n * X ^ (n - 1)) =
    ↑C (↑u⁻¹ * ↑u) - ↑C ↑u⁻¹ * X ^ n + ↑C ↑u⁻¹ * ↑C (n' * ↑n) * (X * X ^ (n - 1))
[PROOFSTEP]
simp only [C.map_mul, C_eq_nat_cast]
[GOAL]
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -↑C ↑u⁻¹ * (X ^ n - ↑C ↑u) + ↑C ↑u⁻¹ * ↑C n' * X * (↑n * X ^ (n - 1)) =
    ↑C ↑u⁻¹ * ↑C ↑u - ↑C ↑u⁻¹ * X ^ n + ↑C ↑u⁻¹ * (↑C n' * ↑n) * (X * X ^ (n - 1))
[PROOFSTEP]
ring
[GOAL]
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ ↑C (↑u⁻¹ * ↑u) - ↑C ↑u⁻¹ * X ^ n + ↑C ↑u⁻¹ * ↑C (n' * ↑n) * (X * X ^ (n - 1)) = 1
[PROOFSTEP]
simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ, Nat.sub_add_cancel (show 1 ≤ n from hpos),
  sub_add_cancel]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
⊢ rootMultiplicity x p ≤ 1
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1
[PROOFSTEP]
rw [rootMultiplicity_eq_multiplicity, dif_neg hp, ← PartENat.coe_le_coe, PartENat.natCast_get, Nat.cast_one]
[GOAL]
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : Separable p
x : R
hp : ¬p = 0
⊢ multiplicity (X - ↑C x) p ≤ 1
[PROOFSTEP]
exact multiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : Separable p
x : R
⊢ Multiset.count x (roots p) ≤ 1
[PROOFSTEP]
rw [count_roots p]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : Separable p
x : R
⊢ rootMultiplicity x p ≤ 1
[PROOFSTEP]
exact rootMultiplicity_le_one_of_separable hsep x
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ f ∣ ↑derivative f
[PROOFSTEP]
conv_lhs => rw [hg3, ← hu]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
| f
[PROOFSTEP]
rw [hg3, ← hu]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
| f
[PROOFSTEP]
rw [hg3, ← hu]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
| f
[PROOFSTEP]
rw [hg3, ← hu]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
h : ↑derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ ↑derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ g * ↑u ∣ ↑derivative f
[PROOFSTEP]
rwa [Units.mul_right_dvd]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F →+* K
p : F[X]
⊢ Separable (map f p) ↔ Separable p
[PROOFSTEP]
simp_rw [separable_def, derivative_map, isCoprime_map]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → f x = f y → x = y
⊢ Separable (∏ i in s, (X - ↑C (f i)))
[PROOFSTEP]
rw [← prod_attach]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → f x = f y → x = y
⊢ Separable (∏ x in attach s, (X - ↑C (f ↑x)))
[PROOFSTEP]
exact
  separable_prod'
    (fun x _hx y _hy hxy =>
      @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x) (fun x y hxy => Subtype.eq <| H x.1 x.2 y.1 y.2 hxy) _
        _ hxy)
    fun _ _ => separable_X_sub_C
[GOAL]
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
ι : Type u_1
inst✝ : Fintype ι
f : ι → F
⊢ (∀ (x : ι), x ∈ univ → ∀ (y : ι), y ∈ univ → f x = f y → x = y) ↔ Function.Injective f
[PROOFSTEP]
simp_rw [mem_univ, true_imp_iff, Function.Injective]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
⊢ Separable f ∨ ¬Separable f ∧ ∃ g, Irreducible g ∧ ↑(expand F p) g = f
[PROOFSTEP]
rcases p.eq_zero_or_pos with (rfl | hp)
[GOAL]
case inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
HF : CharP F 0
⊢ Separable f ∨ ¬Separable f ∧ ∃ g, Irreducible g ∧ ↑(expand F 0) g = f
[PROOFSTEP]
haveI := CharP.charP_to_charZero F
[GOAL]
case inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
HF : CharP F 0
this : CharZero F
⊢ Separable f ∨ ¬Separable f ∧ ∃ g, Irreducible g ∧ ↑(expand F 0) g = f
[PROOFSTEP]
have := natDegree_eq_zero_of_derivative_eq_zero H
[GOAL]
case inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
HF : CharP F 0
this✝ : CharZero F
this : natDegree f = 0
⊢ Separable f ∨ ¬Separable f ∧ ∃ g, Irreducible g ∧ ↑(expand F 0) g = f
[PROOFSTEP]
have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
[GOAL]
case inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
HF : CharP F 0
this✝¹ : CharZero F
this✝ : natDegree f = 0
this : natDegree f ≠ 0
⊢ Separable f ∨ ¬Separable f ∧ ∃ g, Irreducible g ∧ ↑(expand F 0) g = f
[PROOFSTEP]
contradiction
[GOAL]
case inr
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
hp : p > 0
⊢ Separable f ∨ ¬Separable f ∧ ∃ g, Irreducible g ∧ ↑(expand F p) g = f
[PROOFSTEP]
haveI := isLocalRingHom_expand F hp
[GOAL]
case inr
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
hp : p > 0
this : IsLocalRingHom ↑(expand F p)
⊢ Separable f ∨ ¬Separable f ∧ ∃ g, Irreducible g ∧ ↑(expand F p) g = f
[PROOFSTEP]
exact
  Or.inr
    ⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
      of_irreducible_map (expand F p : F[X] →+* F[X]) (by rwa [← expand_contract p H hp.ne'] at hf ),
      expand_contract p H hp.ne'⟩
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
hp : p > 0
this : IsLocalRingHom ↑(expand F p)
⊢ ¬Separable f
[PROOFSTEP]
rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : ↑derivative f = 0
hp : p > 0
this : IsLocalRingHom ↑(expand F p)
⊢ Irreducible (↑↑(expand F p) (contract p f))
[PROOFSTEP]
rwa [← expand_contract p H hp.ne'] at hf
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : p ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : Nat.Prime p
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
induction' hn : f.natDegree using Nat.strong_induction_on with N ih generalizing f
[GOAL]
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
[GOAL]
case h.inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h : Separable f
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
refine' ⟨0, f, h, _⟩
[GOAL]
case h.inl
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h : Separable f
⊢ ↑(expand F (p ^ 0)) f = f
[PROOFSTEP]
rw [pow_zero, expand_one]
[GOAL]
case h.inr.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
N : ℕ
ih : ∀ (m : ℕ), m < N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
f : F[X]
hf : Irreducible f
hn : natDegree f = N
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
cases' N with N
[GOAL]
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.zero
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
[GOAL]
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
[GOAL]
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
have hf0 : f ≠ 0 := hf.ne_zero
[GOAL]
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = ↑C (coeff f 0)
hf0 : f ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
rw [h1, C_0] at hn
[GOAL]
case h.inr.intro.intro.intro.zero
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : coeff f 0 = 0
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
ih :
  ∀ (m : ℕ),
    m < Nat.zero → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : f = 0
hf0 : f ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
exact absurd hn hf0
[GOAL]
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
⊢ natDegree g * p = Nat.succ N
[PROOFSTEP]
rwa [← natDegree_expand, hgf]
[GOAL]
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
have hg2 : g.natDegree ≠ 0 := by
  intro this
  rw [this, zero_mul] at hg1
  cases hg1
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
⊢ natDegree g ≠ 0
[PROOFSTEP]
intro this
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
this : natDegree g = 0
⊢ False
[PROOFSTEP]
rw [this, zero_mul] at hg1
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : 0 = Nat.succ N
this : natDegree g = 0
⊢ False
[PROOFSTEP]
cases hg1
[GOAL]
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
have hg3 : g.natDegree < N.succ := by
  rw [← mul_one g.natDegree, ← hg1]
  exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ natDegree g < Nat.succ N
[PROOFSTEP]
rw [← mul_one g.natDegree, ← hg1]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
⊢ natDegree g * 1 < natDegree g * p
[PROOFSTEP]
exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
[GOAL]
case h.inr.intro.intro.intro.succ
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
g : F[X]
hg : Irreducible g
hgf : ↑(expand F p) g = f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
hg1 : natDegree g * p = Nat.succ N
hg2 : natDegree g ≠ 0
hg3 : natDegree g < Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
[GOAL]
case h.inr.intro.intro.intro.succ.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
n : ℕ
g : F[X]
hg4 : Separable g
hg : Irreducible (↑(expand F (p ^ n)) g)
hgf : ↑(expand F p) (↑(expand F (p ^ n)) g) = f
hg1 : natDegree (↑(expand F (p ^ n)) g) * p = Nat.succ N
hg2 : natDegree (↑(expand F (p ^ n)) g) ≠ 0
hg3 : natDegree (↑(expand F (p ^ n)) g) < Nat.succ N
⊢ ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
[PROOFSTEP]
refine' ⟨n + 1, g, hg4, _⟩
[GOAL]
case h.inr.intro.intro.intro.succ.intro.intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f✝ : F[X]
hf✝ : Irreducible f✝
hp : Nat.Prime p
x✝ : ℕ
hn✝ : natDegree f✝ = x✝
f : F[X]
hf : Irreducible f
h1 : ¬Separable f
N : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ N → ∀ {f : F[X]}, Irreducible f → natDegree f = m → ∃ n g, Separable g ∧ ↑(expand F (p ^ n)) g = f
hn : natDegree f = Nat.succ N
n : ℕ
g : F[X]
hg4 : Separable g
hg : Irreducible (↑(expand F (p ^ n)) g)
hgf : ↑(expand F p) (↑(expand F (p ^ n)) g) = f
hg1 : natDegree (↑(expand F (p ^ n)) g) * p = Nat.succ N
hg2 : natDegree (↑(expand F (p ^ n)) g) ≠ 0
hg3 : natDegree (↑(expand F (p ^ n)) g) < Nat.succ N
⊢ ↑(expand F (p ^ (n + 1))) g = f
[PROOFSTEP]
rw [← hgf, expand_expand, pow_succ]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
⊢ IsUnit f ∨ n = 0
[PROOFSTEP]
rw [or_iff_not_imp_right]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
⊢ ¬n = 0 → IsUnit f
[PROOFSTEP]
rintro hn : n ≠ 0
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
⊢ IsUnit f
[PROOFSTEP]
have hf2 : derivative (expand F (p ^ n) f) = 0 := by
  rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn.bot_lt, zero_mul, mul_zero]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
⊢ ↑derivative (↑(expand F (p ^ n)) f) = 0
[PROOFSTEP]
rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn.bot_lt, zero_mul, mul_zero]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : Separable (↑(expand F (p ^ n)) f)
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
⊢ IsUnit f
[PROOFSTEP]
rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hf : ∃ r, IsUnit r ∧ ↑C r = ↑(expand F (p ^ n)) f
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
⊢ IsUnit f
[PROOFSTEP]
rcases hf with ⟨r, hr, hrf⟩
[GOAL]
case intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : ↑C r = ↑(expand F (p ^ n)) f
⊢ IsUnit f
[PROOFSTEP]
rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf
[GOAL]
case intro.intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
n : ℕ
hp : 0 < p
hn : n ≠ 0
hf2 : ↑derivative (↑(expand F (p ^ n)) f) = 0
r : F
hr : IsUnit r
hrf : f = ↑C r
⊢ IsUnit f
[PROOFSTEP]
rwa [hrf, isUnit_C]
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
n₂ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
revert g₁ g₂
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
clear! K
[GOAL]
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
wlog hn : n₁ ≤ n₂
[GOAL]
case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
this :
  ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]},
    Irreducible f →
      0 < p →
        ∀ (n₁ n₂ : ℕ),
          n₁ ≤ n₂ →
            ∀ (g₁ : F[X]),
              Separable g₁ →
                ↑(expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
intro g₁ hg₁ Hg₁ g₂ hg₂ Hg₂
[GOAL]
case inr
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
this :
  ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : F[X]},
    Irreducible f →
      0 < p →
        ∀ (n₁ n₂ : ℕ),
          n₁ ≤ n₂ →
            ∀ (g₁ : F[X]),
              Separable g₁ →
                ↑(expand F (p ^ n₁)) g₁ = f →
                  ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
hn : ¬n₁ ≤ n₂
g₁ : F[X]
hg₁ : Separable g₁
Hg₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
Hg₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
simpa only [eq_comm] using this p hf hp n₂ n₁ (le_of_not_le hn) g₂ hg₂ Hg₂ g₁ hg₁ Hg₁
[GOAL]
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
have hf0 : f ≠ 0 := hf.ne_zero
[GOAL]
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
hf0 : f ≠ 0
⊢ ∀ (g₁ : F[X]),
    Separable g₁ →
      ↑(expand F (p ^ n₁)) g₁ = f → ∀ (g₂ : F[X]), Separable g₂ → ↑(expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
intros g₁ hg₁ hgf₁ g₂ hg₂ hgf₂
[GOAL]
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : n₁ ≤ n₂
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
rw [le_iff_exists_add] at hn
[GOAL]
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ n₂ : ℕ
hn : ∃ c, n₂ = n₁ + c
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
hgf₂ : ↑(expand F (p ^ n₂)) g₂ = f
⊢ n₁ = n₂ ∧ g₁ = g₂
[PROOFSTEP]
rcases hn with ⟨k, rfl⟩
[GOAL]
case intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hgf₂ : ↑(expand F (p ^ (n₁ + k))) g₂ = f
⊢ n₁ = n₁ + k ∧ g₁ = g₂
[PROOFSTEP]
rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂
[GOAL]
case intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
hf0 : f ≠ 0
g₁ : F[X]
hg₁ : Separable g₁
hgf₁ : ↑(expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hgf₂ : ↑(expand F (p ^ k)) g₂ = g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂
[PROOFSTEP]
subst hgf₂
[GOAL]
case intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
hf0 : f ≠ 0
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
hgf₁ : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂) = f
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) g₂ = g₂
[PROOFSTEP]
subst hgf₁
[GOAL]
case intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂) ≠ 0
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) g₂ = g₂
[PROOFSTEP]
rcases isUnit_or_eq_zero_of_separable_expand p k hp hg₁ with (h | rfl)
[GOAL]
case intro.inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂) ≠ 0
h : IsUnit g₂
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) g₂ = g₂
[PROOFSTEP]
rw [isUnit_iff] at h
[GOAL]
case intro.inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
k : ℕ
hg₁ : Separable (↑(expand F (p ^ k)) g₂)
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) g₂) ≠ 0
h : ∃ r, IsUnit r ∧ ↑C r = g₂
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) g₂ = g₂
[PROOFSTEP]
rcases h with ⟨r, hr, rfl⟩
[GOAL]
case intro.inl.intro.intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : Separable (↑C r)
hg₁ : Separable (↑(expand F (p ^ k)) (↑C r))
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) (↑C r)))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) (↑C r)) ≠ 0
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) (↑C r) = ↑C r
[PROOFSTEP]
simp_rw [expand_C] at hf
[GOAL]
case intro.inl.intro.intro
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : Separable (↑C r)
hg₁ : Separable (↑(expand F (p ^ k)) (↑C r))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ k)) (↑C r)) ≠ 0
hf : Irreducible (↑C r)
⊢ n₁ = n₁ + k ∧ ↑(expand F (p ^ k)) (↑C r) = ↑C r
[PROOFSTEP]
exact absurd (isUnit_C.2 hr) hf.1
[GOAL]
case intro.inr
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂) ≠ 0
⊢ n₁ = n₁ + 0 ∧ ↑(expand F (p ^ 0)) g₂ = g₂
[PROOFSTEP]
rw [add_zero, pow_zero, expand_one]
[GOAL]
case intro.inr
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂) ≠ 0
⊢ n₁ = n₁ ∧ g₂ = g₂
[PROOFSTEP]
constructor
[GOAL]
case intro.inr.left
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂) ≠ 0
⊢ n₁ = n₁
[PROOFSTEP]
rfl
[GOAL]
case intro.inr.right
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : Separable g₂
hg₁ : Separable (↑(expand F (p ^ 0)) g₂)
hf : Irreducible (↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂))
hf0 : ↑(expand F (p ^ n₁)) (↑(expand F (p ^ 0)) g₂) ≠ 0
⊢ g₂ = g₂
[PROOFSTEP]
rfl
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ Separable (X ^ n - 1) ↔ ↑n ≠ 0
[PROOFSTEP]
refine' ⟨_, fun h => separable_X_pow_sub_C_unit 1 (IsUnit.mk0 (↑n) h)⟩
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ Separable (X ^ n - 1) → ↑n ≠ 0
[PROOFSTEP]
rw [separable_def', derivative_sub, derivative_X_pow, derivative_one, sub_zero]
  -- Suppose `(n : F) = 0`, then the derivative is `0`, so `X ^ n - 1` is a unit, contradiction.
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ (∃ a b, a * (X ^ n - 1) + b * (↑C ↑n * X ^ (n - 1)) = 1) → ↑n ≠ 0
[PROOFSTEP]
rintro (h : IsCoprime _ _) hn'
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
h : IsCoprime (X ^ n - 1) (↑C ↑n * X ^ (n - 1))
hn' : ↑n = 0
⊢ False
[PROOFSTEP]
rw [hn', C_0, zero_mul, isCoprime_zero_right] at h
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
h : IsUnit (X ^ n - 1)
hn' : ↑n = 0
⊢ False
[PROOFSTEP]
exact not_isUnit_X_pow_sub_one F n h
[GOAL]
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ Fintype.card ↑(rootSet p K) = natDegree p
[PROOFSTEP]
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
[GOAL]
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ card (Multiset.toFinset (roots (map (algebraMap F K) p))) = natDegree p
[PROOFSTEP]
rw [Multiset.toFinset_card_of_nodup, ← natDegree_eq_card_roots hsplit]
[GOAL]
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ Multiset.Nodup (roots (map (algebraMap F K) p))
[PROOFSTEP]
exact nodup_roots hsep.map
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
⊢ h = ↑C (leadingCoeff h) * (X - ↑C x)
[PROOFSTEP]
have h_ne_zero : h ≠ 0 := by
  rintro rfl
  exact not_separable_zero h_sep
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
⊢ h ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h_sep : Separable 0
h_root : eval x 0 = 0
h_splits : Splits i 0
h_roots : ∀ (y : K), y ∈ roots (map i 0) → y = ↑i x
⊢ False
[PROOFSTEP]
exact not_separable_zero h_sep
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ h = ↑C (leadingCoeff h) * (X - ↑C x)
[PROOFSTEP]
apply Polynomial.eq_X_sub_C_of_splits_of_single_root i h_splits
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ roots (map i h) = {↑i x}
[PROOFSTEP]
apply Finset.mk.inj
[GOAL]
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ { val := roots (map i h), nodup := ?nodup } = { val := {↑i x}, nodup := ?nodup }
[PROOFSTEP]
change _ = {i x}
[GOAL]
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ { val := roots (map i h), nodup := ?nodup } = {↑i x}
[PROOFSTEP]
rw [Finset.eq_singleton_iff_unique_mem]
[GOAL]
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ { val := roots (map i h), nodup := ?nodup } ∧
    ∀ (x_1 : K), x_1 ∈ { val := roots (map i h), nodup := ?nodup } → x_1 = ↑i x
case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))
[PROOFSTEP]
constructor
[GOAL]
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ { val := roots (map i h), nodup := ?nodup }
[PROOFSTEP]
apply Finset.mem_mk.mpr
[GOAL]
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ roots (map i h)
[PROOFSTEP]
rw [mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)]
[GOAL]
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ IsRoot (map i h) (↑i x)
[PROOFSTEP]
rw [IsRoot.def, ← eval₂_eq_eval_map, eval₂_hom, h_root]
[GOAL]
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i 0 = 0
[PROOFSTEP]
exact RingHom.map_zero i
[GOAL]
case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))
[PROOFSTEP]
exact nodup_roots (Separable.map h_sep)
[GOAL]
case x.right
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ∀ (x_1 : K), x_1 ∈ { val := roots (map i h), nodup := (_ : Multiset.Nodup (roots (map i h))) } → x_1 = ↑i x
[PROOFSTEP]
exact h_roots
[GOAL]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
⊢ ∃ s, map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in s, (X - ↑C a)
[PROOFSTEP]
obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp
[GOAL]
case intro
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ ∃ s, map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in s, (X - ↑C a)
[PROOFSTEP]
use s.toFinset
[GOAL]
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ map i f = ↑C (↑i (leadingCoeff f)) * ∏ a in Multiset.toFinset s, (X - ↑C a)
[PROOFSTEP]
rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq]
[GOAL]
case h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Multiset.Nodup s
[PROOFSTEP]
apply nodup_of_separable_prod
[GOAL]
case h.hs
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
[PROOFSTEP]
apply Separable.of_mul_right
[GOAL]
case h.hs.h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (?h.hs.f * Multiset.prod (Multiset.map (fun a => X - ↑C a) s))
case h.hs.f
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ K[X]
[PROOFSTEP]
rw [← h]
[GOAL]
case h.hs.h
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i✝ i : F →+* K
f : F[X]
sep : Separable f
sp : Splits i f
s : Multiset K
h : map i f = ↑C (↑i (leadingCoeff f)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
⊢ Separable (map i f)
[PROOFSTEP]
exact sep.map
[GOAL]
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ Separable f
[PROOFSTEP]
rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]
[GOAL]
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬↑(natDegree f - 1) = ⊥
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case hp
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ 0 < natDegree f
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne, natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff]
[GOAL]
case hp
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬f = ↑C (coeff f 0)
[PROOFSTEP]
refine' fun hf1 => hf.not_unit _
[GOAL]
case hp
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = ↑C (coeff f 0)
⊢ IsUnit f
[PROOFSTEP]
rw [hf1, isUnit_C, isUnit_iff_ne_zero]
[GOAL]
case hp
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = ↑C (coeff f 0)
⊢ coeff f 0 ≠ 0
[PROOFSTEP]
intro hf2
[GOAL]
case hp
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = ↑C (coeff f 0)
hf2 : coeff f 0 = 0
⊢ False
[PROOFSTEP]
rw [hf2, C_0] at hf1
[GOAL]
case hp
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
hf1 : f = 0
hf2 : coeff f 0 = 0
⊢ False
[PROOFSTEP]
exact absurd hf1 hf.ne_zero
[GOAL]
F : Type u_1
inst✝ : Field F
x : F
⊢ Separable (minpoly F x)
[PROOFSTEP]
rw [minpoly.eq_X_sub_C']
[GOAL]
F : Type u_1
inst✝ : Field F
x : F
⊢ Separable (X - ↑C x)
[PROOFSTEP]
exact separable_X_sub_C
[GOAL]
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
⊢ IsIntegral F x ∧ Separable (minpoly F x)
[PROOFSTEP]
refine' (isSeparable_iff.1 h (algebraMap K E x)).imp isIntegral_tower_bot_of_isIntegral_field fun hs => _
[GOAL]
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
hs : Separable (minpoly F (↑(algebraMap K E) x))
⊢ Separable (minpoly F x)
[PROOFSTEP]
obtain ⟨q, hq⟩ := minpoly.dvd F x ((aeval_algebraMap_eq_zero_iff _ _ _).mp (minpoly.aeval F ((algebraMap K E) x)))
[GOAL]
case intro
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
hs : Separable (minpoly F (↑(algebraMap K E) x))
q : F[X]
hq : minpoly F (↑(algebraMap K E) x) = minpoly F x * q
⊢ Separable (minpoly F x)
[PROOFSTEP]
rw [hq] at hs
[GOAL]
case intro
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field E
inst✝³ : Algebra F K
inst✝² : Algebra F E
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
h : IsSeparable F E
x : K
q : F[X]
hs : Separable (minpoly F x * q)
hq : minpoly F (↑(algebraMap K E) x) = minpoly F x * q
⊢ Separable (minpoly F x)
[PROOFSTEP]
exact hs.of_mul_left
[GOAL]
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Field E
inst✝⁶ : Algebra F K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra K E
inst✝³ : IsScalarTower F K E
E' : Type u_4
inst✝² : Field E'
inst✝¹ : Algebra F E'
f : E →ₐ[F] E'
inst✝ : IsSeparable F E'
⊢ IsSeparable F E
[PROOFSTEP]
letI : Algebra E E' := RingHom.toAlgebra f.toRingHom
[GOAL]
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Field E
inst✝⁶ : Algebra F K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra K E
inst✝³ : IsScalarTower F K E
E' : Type u_4
inst✝² : Field E'
inst✝¹ : Algebra F E'
f : E →ₐ[F] E'
inst✝ : IsSeparable F E'
this : Algebra E E' := RingHom.toAlgebra ↑f
⊢ IsSeparable F E
[PROOFSTEP]
haveI : IsScalarTower F E E' := IsScalarTower.of_algebraMap_eq fun x => (f.commutes x).symm
[GOAL]
F : Type u_1
K : Type u_2
E : Type u_3
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Field E
inst✝⁶ : Algebra F K
inst✝⁵ : Algebra F E
inst✝⁴ : Algebra K E
inst✝³ : IsScalarTower F K E
E' : Type u_4
inst✝² : Field E'
inst✝¹ : Algebra F E'
f : E →ₐ[F] E'
inst✝ : IsSeparable F E'
this✝ : Algebra E E' := RingHom.toAlgebra ↑f
this : IsScalarTower F E E'
⊢ IsSeparable F E
[PROOFSTEP]
exact isSeparable_tower_bot_of_isSeparable F E E'
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing S
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
[PROOFSTEP]
let s := ((minpoly K pb.gen).map (algebraMap K L)).roots.toFinset
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing S
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
[PROOFSTEP]
let _ := (PowerBasis.AlgHom.fintype pb : Fintype (S →ₐ[K] L))
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing S
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
[PROOFSTEP]
rw [Fintype.card_congr pb.liftEquiv', Fintype.card_of_subtype s (fun x => Multiset.mem_toFinset), ←
  pb.natDegree_minpoly, natDegree_eq_card_roots h_splits, Multiset.toFinset_card_of_nodup]
[GOAL]
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing S
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field F
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : Separable (minpoly K pb.gen)
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
s : Finset L := Multiset.toFinset (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Multiset.Nodup (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen)))
[PROOFSTEP]
exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)


[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
[PROOFSTEP]
have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
this : r = p
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
[PROOFSTEP]
subst this
[GOAL]
α✝ : Sort u_1
β : Sort u_2
α : Sort u_3
r : α → α → Prop
iseqv✝¹ iseqv✝ : Equivalence r
Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := r, iseqv := iseqv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : (a : α) → (b : β) → φ (mk ra a) (mk rb b)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → HEq (f a₁ b) (f a₂ b)
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a b₁) (f a b₂)
a₁ a₂ : α
pa : ra a₁ a₂
b : β
⊢ HEq (Quot.hrecOn (mk rb b) (f a₁) (_ : ∀ {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a₁ b₁) (f a₁ b₂))) (f a₁ b)
[PROOFSTEP]
simp [heq_self_iff_true]
[GOAL]
α : Sort u_1
β : Sort u_2
ra : α → α → Prop
rb : β → β → Prop
φ : Quot ra → Quot rb → Sort u_3
qa : Quot ra
qb : Quot rb
f : (a : α) → (b : β) → φ (mk ra a) (mk rb b)
ca : ∀ {b : β} {a₁ a₂ : α}, ra a₁ a₂ → HEq (f a₁ b) (f a₂ b)
cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a b₁) (f a b₂)
a₁ a₂ : α
pa : ra a₁ a₂
b : β
h₁ : HEq (Quot.hrecOn (mk rb b) (f a₁) (_ : ∀ {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a₁ b₁) (f a₁ b₂))) (f a₁ b)
⊢ HEq (f a₂ b) (Quot.hrecOn (mk rb b) (f a₂) (_ : ∀ {b₁ b₂ : β}, rb b₁ b₂ → HEq (f a₂ b₁) (f a₂ b₂)))
[PROOFSTEP]
simp [heq_self_iff_true]
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : α
y : Quotient s
⊢ Quotient.mk s x = y ↔ x ≈ out y
[PROOFSTEP]
refine' Iff.trans _ Quotient.eq
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : α
y : Quotient s
⊢ Quotient.mk s x = y ↔ Quotient.mk s x = Quotient.mk s (out y)
[PROOFSTEP]
rw [Quotient.out_eq y]
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : Quotient s
y : α
⊢ x = Quotient.mk s y ↔ out x ≈ y
[PROOFSTEP]
refine' Iff.trans _ Quotient.eq
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x : Quotient s
y : α
⊢ x = Quotient.mk s y ↔ Quotient.mk s (out x) = Quotient.mk s y
[PROOFSTEP]
rw [Quotient.out_eq x]
[GOAL]
α : Sort u_1
β : Sort u_2
s : Setoid α
x y : Quotient s
⊢ out x ≈ out y ↔ x = y
[PROOFSTEP]
rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Type u_4
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
⊢ Setoid ((i : ι) → α i)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => Quotient.mk (s i) (a i)
⊢ p f
[PROOFSTEP]
rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
ι : Type u_3
α : ι → Sort u_4
s : (i : ι) → Setoid (α i)
p : ((i : ι) → Quotient (s i)) → Prop
f : (i : ι) → Quotient (s i)
h : ∀ (a : (i : ι) → α i), p fun i => Quotient.mk (s i) (a i)
⊢ p fun i => Quotient.mk (s i) (out (f i))
[PROOFSTEP]
apply h


[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic (minpoly A x)
[PROOFSTEP]
delta minpoly
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (if hx : IsIntegral A x then
      WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
    else 0)
[PROOFSTEP]
rw [dif_pos hx]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ Monic
    (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx)
[PROOFSTEP]
exact (degree_lt_wf.min_mem _ hx).1
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x✝ : B
f : B →ₐ[A] B'
hf : Injective ↑f
x : B
⊢ minpoly A (↑f x) = minpoly A x
[PROOFSTEP]
refine' dif_ctx_congr (isIntegral_algHom_iff _ hf) (fun _ => _) fun _ => rfl
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x✝¹ : B
f : B →ₐ[A] B'
hf : Injective ↑f
x : B
x✝ : IsIntegral A x
⊢ WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A ((fun x => B') x)) (↑f x) x_1 = 0) (_ : IsIntegral A (↑f x)) =
    WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
      (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) x✝
[PROOFSTEP]
simp_rw [← Polynomial.aeval_def, aeval_algHom, AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
⊢ ↑(Polynomial.aeval x) (minpoly A x) = 0
[PROOFSTEP]
delta minpoly
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
⊢ ↑(Polynomial.aeval x)
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) =
    0
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) =
    0
[PROOFSTEP]
rw [dif_pos hx]
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) =
    0
[PROOFSTEP]
exact (degree_lt_wf.min_mem _ hx).2
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x)
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) =
    0
[PROOFSTEP]
rw [dif_neg hx]
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ¬IsIntegral A x
⊢ ↑(Polynomial.aeval x) 0 = 0
[PROOFSTEP]
exact aeval_zero _
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
⊢ minpoly A x ≠ 1
[PROOFSTEP]
intro h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False
[PROOFSTEP]
refine' (one_ne_zero : (1 : B) ≠ 0) _
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 0
[PROOFSTEP]
simpa using congr_arg (Polynomial.aeval x) h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
⊢ map f (minpoly A x) ≠ 1
[PROOFSTEP]
by_cases hx : IsIntegral A x
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
[PROOFSTEP]
exact mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x)
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1
[PROOFSTEP]
rw [eq_zero hx, Polynomial.map_zero]
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : Ring B'
inst✝⁴ : Algebra A B
inst✝³ : Algebra A B'
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ 0 ≠ 1
[PROOFSTEP]
exact zero_ne_one
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
haveI : Nontrivial A := (algebraMap A B).domain_nontrivial
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
by_cases hx : IsIntegral A x
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : IsIntegral A x
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
exact mt (monic hx).eq_one_of_isUnit (ne_one A x)
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit (minpoly A x)
[PROOFSTEP]
rw [eq_zero hx]
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Nontrivial B
this : Nontrivial A
hx : ¬IsIntegral A x
⊢ ¬IsUnit 0
[PROOFSTEP]
exact not_isUnit_zero
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
have h : IsIntegral A x := by
  by_contra h
  rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
  exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
⊢ IsIntegral A x
[PROOFSTEP]
by_contra h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : ¬IsIntegral A x
⊢ False
[PROOFSTEP]
rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : ⊥ = ↑1
h : ¬IsIntegral A x
⊢ False
[PROOFSTEP]
exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
have key := minpoly.aeval A x
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : ↑(Polynomial.aeval x) (minpoly A x) = 0
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add, aeval_C, aeval_X, ←
  eq_neg_iff_add_eq_zero, ← RingHom.map_neg] at key
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
hx : degree (minpoly A x) = 1
h : IsIntegral A x
key : x = ↑(algebraMap A B) (-coeff (minpoly A x) 0)
⊢ x ∈ RingHom.range (algebraMap A B)
[PROOFSTEP]
exact ⟨-(minpoly A x).coeff 0, key.symm⟩
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
⊢ degree (minpoly A x) ≤ degree p
[PROOFSTEP]
delta minpoly
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
⊢ degree
      (if hx : IsIntegral A x then
        WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
          (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx
      else 0) ≤
    degree p
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : IsIntegral A x
⊢ degree
      (WellFounded.min (_ : WellFounded fun p q => degree p < degree q)
        (fun x_1 => Monic x_1 ∧ eval₂ (algebraMap A B) x x_1 = 0) hx) ≤
    degree p
[PROOFSTEP]
exact le_of_not_lt (degree_lt_wf.not_lt_min _ hx ⟨pmonic, hp⟩)
[GOAL]
case neg
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
pmonic : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hx : ¬IsIntegral A x
⊢ degree 0 ≤ degree p
[PROOFSTEP]
simp only [degree_zero, bot_le]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
⊢ p = minpoly A x
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
⊢ p = minpoly A x
[PROOFSTEP]
have hx : IsIntegral A x := ⟨p, hm, hp⟩
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
⊢ p = minpoly A x
[PROOFSTEP]
obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x
[PROOFSTEP]
swap
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : ↑(Polynomial.aeval x) (minpoly A x %ₘ p) ≠ 0
⊢ p = minpoly A x
[PROOFSTEP]
exact (h <| (aeval_modByMonic_eq_self_of_root hm hp).trans <| aeval A x).elim
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
⊢ p = minpoly A x
[PROOFSTEP]
obtain ⟨r, hr⟩ := (dvd_iff_modByMonic_eq_zero hm).1 h
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = minpoly A x
[PROOFSTEP]
rw [hr]
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
⊢ p = p * r
[PROOFSTEP]
have hlead := congr_arg leadingCoeff hr
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : leadingCoeff (minpoly A x) = leadingCoeff (p * r)
⊢ p = p * r
[PROOFSTEP]
rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ p = p * r
[PROOFSTEP]
have : natDegree r ≤ 0 :=
  by
  have hr0 : r ≠ 0 := by
    rintro rfl
    exact ne_zero hx (mul_zero p ▸ hr)
  apply_fun natDegree at hr
  rw [hm.natDegree_mul' hr0] at hr
  apply Nat.le_of_add_le_add_left
  rw [add_zero]
  exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ natDegree r ≤ 0
[PROOFSTEP]
have hr0 : r ≠ 0 := by
  rintro rfl
  exact ne_zero hx (mul_zero p ▸ hr)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
⊢ r ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
hr : minpoly A x = p * 0
hlead : 1 = leadingCoeff 0
⊢ False
[PROOFSTEP]
exact ne_zero hx (mul_zero p ▸ hr)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
⊢ natDegree r ≤ 0
[PROOFSTEP]
apply_fun natDegree at hr
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree (p * r)
⊢ natDegree r ≤ 0
[PROOFSTEP]
rw [hm.natDegree_mul' hr0] at hr
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ natDegree r ≤ 0
[PROOFSTEP]
apply Nat.le_of_add_le_add_left
[GOAL]
case h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?a + natDegree r ≤ ?a + 0
case a
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
[PROOFSTEP]
rw [add_zero]
[GOAL]
case h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ?h + natDegree r ≤ ?h
case h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hlead : 1 = leadingCoeff r
hr0 : r ≠ 0
hr : natDegree (minpoly A x) = natDegree p + natDegree r
⊢ ℕ
[PROOFSTEP]
exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
[GOAL]
case inl.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
x : B
p : A[X]
hm : Monic p
hp : ↑(Polynomial.aeval x) p = 0
hl : ∀ (q : A[X]), degree q < degree p → q = 0 ∨ ↑(Polynomial.aeval x) q ≠ 0
✝ : Nontrivial A
hx : IsIntegral A x
h : minpoly A x %ₘ p = 0
r : A[X]
hr : minpoly A x = p * r
hlead : 1 = leadingCoeff r
this : natDegree r ≤ 0
⊢ p = p * r
[PROOFSTEP]
rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1, mul_one]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
⊢ minpoly A x = 1
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
⊢ minpoly A x = 1
[PROOFSTEP]
have := minpoly.min A x monic_one (Subsingleton.elim _ _)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ degree 1
⊢ minpoly A x = 1
[PROOFSTEP]
rw [degree_one] at this
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1
[PROOFSTEP]
cases' le_or_lt (minpoly A x).degree 0 with h h
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ minpoly A x = 1
[PROOFSTEP]
rwa [(monic ⟨1, monic_one, by simp⟩ : (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : degree (minpoly A x) ≤ 0
⊢ eval₂ (algebraMap A B) x 1 = 0
[PROOFSTEP]
simp
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Ring B'
inst✝² : Algebra A B
inst✝¹ : Algebra A B'
x : B
inst✝ : Subsingleton B
✝ : Nontrivial A
this : degree (minpoly A x) ≤ 0
h : 0 < degree (minpoly A x)
⊢ minpoly A x = 1
[PROOFSTEP]
exact (this.not_lt h).elim
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ 0 < natDegree (minpoly A x)
[PROOFSTEP]
rw [pos_iff_ne_zero]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ natDegree (minpoly A x) ≠ 0
[PROOFSTEP]
intro ndeg_eq_zero
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ False
[PROOFSTEP]
have eq_one : minpoly A x = 1 := by
  rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
  convert C_1 (R := A)
  simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ minpoly A x = 1
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ ↑C (coeff (minpoly A x) 0) = 1
[PROOFSTEP]
convert C_1 (R := A)
[GOAL]
case h.e'_2.h.e'_6
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
⊢ coeff (minpoly A x) 0 = 1
[PROOFSTEP]
simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : natDegree (minpoly A x) = 0
eq_one : minpoly A x = 1
⊢ False
[PROOFSTEP]
simpa only [eq_one, AlgHom.map_one, one_ne_zero] using aeval A x
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
⊢ minpoly A (↑(algebraMap A B) a) = X - ↑C a
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ minpoly A (↑(algebraMap A B) a) = X - ↑C a
[PROOFSTEP]
refine' (unique' A _ (monic_X_sub_C a) _ _).symm
[GOAL]
case refine'_1
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (X - ↑C a) = 0
[PROOFSTEP]
rw [map_sub, aeval_C, aeval_X, sub_self]
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → q = 0 ∨ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
simp_rw [or_iff_not_imp_left]
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
⊢ ∀ (q : A[X]), degree q < degree (X - ↑C a) → ¬q = 0 → ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
intro q hl h0
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : degree q < degree (X - ↑C a)
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬q = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) q ≠ 0
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hl] at h0 ⊢
[GOAL]
case refine'_2
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A
hf : Injective ↑(algebraMap A B)
✝ : Nontrivial A
q : A[X]
hl : natDegree q = 0
h0 : ¬↑C (coeff q 0) = 0
⊢ ↑(Polynomial.aeval (↑(algebraMap A B) a)) (↑C (coeff q 0)) ≠ 0
[PROOFSTEP]
rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
hdvd : DvdNotUnit a (minpoly A x)
⊢ ↑(Polynomial.aeval x) a ≠ 0
[PROOFSTEP]
refine' fun ha => (min A x hamonic ha).not_lt (degree_lt_degree _)
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
hdvd : DvdNotUnit a (minpoly A x)
ha : ↑(Polynomial.aeval x) a = 0
⊢ natDegree a < natDegree (minpoly A x)
[PROOFSTEP]
obtain ⟨_, c, hu, he⟩ := hdvd
[GOAL]
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ natDegree a < natDegree (minpoly A x)
[PROOFSTEP]
have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)
[GOAL]
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree (minpoly A x)
[PROOFSTEP]
rw [he, hamonic.natDegree_mul hcm]
  -- TODO: port Nat.lt_add_of_zero_lt_left from lean3 core
[GOAL]
case intro.intro.intro
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ natDegree a < natDegree a + natDegree c
[PROOFSTEP]
apply lt_add_of_pos_right
[GOAL]
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
⊢ 0 < natDegree c
[PROOFSTEP]
refine (lt_of_not_le fun h => hu ?_)
[GOAL]
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit c
[PROOFSTEP]
rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff, C_1]
[GOAL]
case intro.intro.intro.h
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : Monic a
ha : ↑(Polynomial.aeval x) a = 0
left✝ : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : Monic c
h : natDegree c ≤ 0
⊢ IsUnit 1
[PROOFSTEP]
exact isUnit_one
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
⊢ Irreducible (minpoly A x)
[PROOFSTEP]
refine' (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => _
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
rw [← hf.isUnit_iff, ← hg.isUnit_iff]
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
⊢ IsUnit f ∨ IsUnit g
[PROOFSTEP]
by_contra' h
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
⊢ False
[PROOFSTEP]
have heval := congr_arg (Polynomial.aeval x) he
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) (f * g) = ↑(Polynomial.aeval x) (minpoly A x)
⊢ False
[PROOFSTEP]
rw [aeval A x, aeval_mul, mul_eq_zero] at heval
[GOAL]
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0 ∨ ↑(Polynomial.aeval x) g = 0
⊢ False
[PROOFSTEP]
cases' heval with heval heval
[GOAL]
case inl
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) f = 0
⊢ False
[PROOFSTEP]
exact aeval_ne_zero_of_dvdNotUnit_minpoly hx hf ⟨hf.ne_zero, g, h.2, he.symm⟩ heval
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ False
[PROOFSTEP]
refine' aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, _⟩ heval
[GOAL]
case inr
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : Monic f
hg : Monic g
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : ↑(Polynomial.aeval x) g = 0
⊢ minpoly A x = g * f
[PROOFSTEP]
rw [mul_comm, he]