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

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
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
rcases p.eq_zero_or_pos with (rfl | hp)
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
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
haveI := isLocalRingHom_expand F hp
no goals
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
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'⟩
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
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
haveI := CharP.charP_to_charZero F
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
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
have := natDegree_eq_zero_of_derivative_eq_zero H
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
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
have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
no goals
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
contradiction
no goals
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
rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H]
no goals
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))
rwa [← expand_contract p H hp.ne'] at hf