F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬↑(natDegree f - 1) = ⊥

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
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ Separable f
rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]
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)
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
rw [pos_iff_ne_zero, Ne, natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff]
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
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)
refine' fun hf1 => hf.not_unit _
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
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
rw [hf1, isUnit_C, isUnit_iff_ne_zero]
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
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
intro hf2
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
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
rw [hf2, C_0] at hf1
no goals
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
exact absurd hf1 hf.ne_zero
no goals
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬↑(natDegree f - 1) = ⊥
rintro ⟨⟩