-- Mathlib/FieldTheory/SeparableDegree.lean
theorem perfectField_iff_splits_of_natSepDegree_eq_one (F : Type*) [Field F] :
    PerfectField F ↔ ∀ f : F[X], f.natSepDegree = 1 → f.Splits (RingHom.id F)

Proof state:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ f
this : g.natDegree ≤ 1
⊢ g.degree = 1

Tactic:
exact (degree_eq_iff_natDegree_eq_of_pos one_pos).2 <| this.antisymm <|
  natDegree_pos_iff_degree_pos.2 (degree_pos_of_irreducible hg)

Result:
no goals

Proof state:
case refine_2
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
⊢ PerfectField F

Tactic:
obtain ⟨p, _⟩ := ExpChar.exists F

Result:
case refine_2.intro
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
⊢ PerfectField F

Proof state:
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
x y : F
hy : eval₂ (RingHom.id F) y (X ^ p - C x) = 0
⊢ (frobenius F p) y = x

Tactic:
rwa [← eval, eval_sub, eval_pow, eval_X, eval_C, sub_eq_zero] at hy

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
x : F
⊢ ∃ a, (frobenius F p) a = x

Tactic:
obtain ⟨y, hy⟩ := exists_root_of_splits _
  (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
  ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'

Result:
case intro
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
x y : F
hy : eval₂ (RingHom.id F) y (X ^ p - C x) = 0
⊢ ∃ a, (frobenius F p) a = x

Proof state:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ f
⊢ g.degree = 1

Tactic:
have := natSepDegree_le_of_dvd g f hd hn

Result:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ f
this : g.natSepDegree ≤ f.natSepDegree
⊢ g.degree = 1

Proof state:
case refine_2.intro
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
⊢ PerfectField F

Tactic:
haveI := PerfectRing.ofSurjective F p fun x ↦ by
  obtain ⟨y, hy⟩ := exists_root_of_splits _
    (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
    ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'
  exact ⟨y, by rwa [← eval, eval_sub, eval_pow, eval_X, eval_C, sub_eq_zero] at hy⟩

Result:
case refine_2.intro
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
this : PerfectRing F p
⊢ PerfectField F

Proof state:
F : Type u_1
inst✝ : Field F
⊢ PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f

Tactic:
refine ⟨fun ⟨h⟩ f hf ↦ or_iff_not_imp_left.2 fun hn g hg hd ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬Polynomial.map (RingHom.id F) f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ Polynomial.map (RingHom.id F) f
⊢ g.degree = 1

case refine_2
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
⊢ PerfectField F

Proof state:
case intro
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
x y : F
hy : eval₂ (RingHom.id F) y (X ^ p - C x) = 0
⊢ ∃ a, (frobenius F p) a = x

Tactic:
exact ⟨y, by rwa [← eval, eval_sub, eval_pow, eval_X, eval_C, sub_eq_zero] at hy⟩

Result:
no goals

Proof state:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ f
this : g.natSepDegree ≤ f.natSepDegree
⊢ g.degree = 1

Tactic:
rw [hf, (h hg).natSepDegree_eq_natDegree] at this

Result:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ f
this : g.natDegree ≤ 1
⊢ g.degree = 1

Proof state:
case refine_2.intro
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → Splits (RingHom.id F) f
p : ℕ
h✝ : ExpChar F p
this : PerfectRing F p
⊢ PerfectField F

Tactic:
exact PerfectRing.toPerfectField F p

Result:
no goals

Proof state:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬Polynomial.map (RingHom.id F) f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ Polynomial.map (RingHom.id F) f
⊢ g.degree = 1

Tactic:
rw [map_id] at hn hd

Result:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hn : ¬f = 0
g : F[X]
hg : Irreducible g
hd : g ∣ f
⊢ g.degree = 1