still depends on #9522

Mathlib/FieldTheory/IsSepClosed.lean

@@ -26,6 +26,9 @@ and prove some of their properties.
 - `IsSepClosure.equiv` is a proof that any two separable closures of the
   same field are isomorphic.
 
+- `IsSepClosure.isAlgClosure_of_perfectField`, `IsSepClosure.of_isAlgClosure_of_perfectField`:
+  if `k` is a perfect field, then its separable closure coincides with its algebraic closure.
+
 ## Tags
 
 separable closure, separably closed
@@ -40,11 +43,8 @@ separable closure, separably closed
 
 - In particular, a separable closure (`SeparableClosure`) exists.
 
-## TODO
-
-- If `k` is a perfect field, then its separable closure coincides with its algebraic closure.
-
-- An algebraic extension of a separably closed field is purely inseparable.
+- `Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed`: an algebraic extension of a separably
+  closed field is purely inseparable.
 
 -/
 
@@ -94,6 +94,13 @@ theorem exists_root [IsSepClosed k] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.S
     ∃ x, IsRoot p x :=
   exists_root_of_splits _ (IsSepClosed.splits_of_separable p hsep) hp
 
+variable (k) in
+/-- A separably closed perfect field is also algebraically closed. -/
+instance (priority := 100) isAlgClosed_of_perfectField [IsSepClosed k] [PerfectField k] :
+    IsAlgClosed k :=
+  IsAlgClosed.of_exists_root k fun p _ h ↦ exists_root p ((degree_pos_of_irreducible h).ne')
+    (PerfectField.separable_of_irreducible h)
+
 theorem exists_pow_nat_eq [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero (n : k)] :
     ∃ z, z ^ n = x := by
   have hn' : 0 < n := Nat.pos_of_ne_zero fun h => by
@@ -191,6 +198,27 @@ class IsSepClosure [Algebra k K] : Prop where
 instance IsSepClosure.self_of_isSepClosed [IsSepClosed k] : IsSepClosure k k :=
   ⟨by assumption, isSeparable_self k⟩
 
+/-- If `K` is perfect and is a separable closure of `k`,
+then it is also an algebraic closure of `k`. -/
+instance (priority := 100) IsSepClosure.isAlgClosure_of_perfectField_top
+    [Algebra k K] [IsSepClosure k K] [PerfectField K] : IsAlgClosure k K :=
+  haveI : IsSepClosed K := IsSepClosure.sep_closed k
+  ⟨inferInstance, IsSepClosure.separable.isAlgebraic⟩
+
+/-- If `k` is perfect, `K` is a separable closure of `k`,
+then it is also an algebraic closure of `k`. -/
+instance (priority := 100) IsSepClosure.isAlgClosure_of_perfectField
+    [Algebra k K] [IsSepClosure k K] [PerfectField k] : IsAlgClosure k K :=
+  have halg : Algebra.IsAlgebraic k K := IsSepClosure.separable.isAlgebraic
+  haveI := halg.perfectField; inferInstance
+
+/-- If `k` is perfect, `K` is an algebraic closure of `k`,
+then it is also a separable closure of `k`. -/
+instance (priority := 100) IsSepClosure.of_isAlgClosure_of_perfectField
+    [Algebra k K] [IsAlgClosure k K] [PerfectField k] : IsSepClosure k K :=
+  ⟨haveI := IsAlgClosure.alg_closed (R := k) (K := K); inferInstance,
+    (IsAlgClosure.algebraic (R := k) (K := K)).isSeparable_of_perfectField⟩
+
 variable {k} {K}
 
 theorem isSepClosure_iff [Algebra k K] :

Mathlib/FieldTheory/Perfect.lean

@@ -218,3 +218,17 @@ instance toPerfectRing (p : ℕ) [hp : Fact p.Prime] [CharP K p] : PerfectRing K
   exact minpoly.degree_pos ha
 
 end PerfectField
+
+/-- If `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable. -/
+theorem Algebra.IsAlgebraic.isSeparable_of_perfectField {K L : Type*} [Field K] [Field L]
+    [Algebra K L] [PerfectField K] (halg : Algebra.IsAlgebraic K L) : IsSeparable K L :=
+  ⟨fun x ↦ PerfectField.separable_of_irreducible <| minpoly.irreducible (halg x).isIntegral⟩
+
+/-- If `L / K` is an algebraic extension, `K` is a perfect field, then so is `L`. -/
+theorem Algebra.IsAlgebraic.perfectField {K L : Type*} [Field K] [Field L] [Algebra K L]
+    [PerfectField K] (halg : Algebra.IsAlgebraic K L) : PerfectField L := ⟨fun {f} hf ↦
+  haveI := Fact.mk hf
+  have h := hf.ne_zero
+  have h2 := isIntegral_trans halg.isIntegral _ (AdjoinRoot.isIntegral_root h)
+  have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
+  (PerfectField.separable_of_irreducible (minpoly.irreducible h2)).map |>.of_dvd h3 |>.of_mul_left⟩