diff --git a/Mathlib/Data/Fintype/Order.lean b/Mathlib/Data/Fintype/Order.lean
index 6fa3b6c7e32fd..127472ab51f1d 100644
--- a/Mathlib/Data/Fintype/Order.lean
+++ b/Mathlib/Data/Fintype/Order.lean
@@ -6,6 +6,7 @@ Authors: Peter Nelson, Yaël Dillies
 import Mathlib.Data.Finset.Order
 import Mathlib.Order.Atoms
 import Mathlib.Data.Set.Finite
+import Mathlib.Order.Minimal
 
 /-!
 # Order structures on finite types
diff --git a/Mathlib/Order/CompleteLattice/Finset.lean b/Mathlib/Order/CompleteLattice/Finset.lean
index b96b173756c62..b02e5eb918efa 100644
--- a/Mathlib/Order/CompleteLattice/Finset.lean
+++ b/Mathlib/Order/CompleteLattice/Finset.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Finset.Option
-import Mathlib.Order.Minimal
+import Mathlib.Data.Set.Lattice
 
 /-!
 # Lattice operations on finsets
diff --git a/Mathlib/Order/Defs.lean b/Mathlib/Order/Defs.lean
index a6a6ffa250fe6..7a46f0ce76cf7 100644
--- a/Mathlib/Order/Defs.lean
+++ b/Mathlib/Order/Defs.lean
@@ -184,6 +184,32 @@ end
 
 end
 
+/-! ### Minimal and maximal -/
+
+section LE
+
+variable {α : Type*} [LE α] {P : α → Prop} {x y : α}
+
+/-- `Minimal P x` means that `x` is a minimal element satisfying `P`. -/
+def Minimal (P : α → Prop) (x : α) : Prop := P x ∧ ∀ ⦃y⦄, P y → y ≤ x → x ≤ y
+
+/-- `Maximal P x` means that `x` is a maximal element satisfying `P`. -/
+def Maximal (P : α → Prop) (x : α) : Prop := P x ∧ ∀ ⦃y⦄, P y → x ≤ y → y ≤ x
+
+lemma Minimal.prop (h : Minimal P x) : P x :=
+  h.1
+
+lemma Maximal.prop (h : Maximal P x) : P x :=
+  h.1
+
+lemma Minimal.le_of_le (h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y :=
+  h.2 hy hle
+
+lemma Maximal.le_of_ge (h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x :=
+  h.2 hy hge
+
+end LE
+
 /-! ### Bundled classes -/
 
 variable {α : Type*}
diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean
index f393265bd856c..18b4a5cf5790c 100644
--- a/Mathlib/Order/Filter/AtTopBot.lean
+++ b/Mathlib/Order/Filter/AtTopBot.lean
@@ -8,6 +8,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.Filter.Bases
 import Mathlib.Order.Filter.Prod
 import Mathlib.Order.Interval.Set.Disjoint
+import Mathlib.Order.Interval.Set.OrderIso
 
 /-!
 # `Filter.atTop` and `Filter.atBot` filters on preorders, monoids and groups.
diff --git a/Mathlib/Order/Minimal.lean b/Mathlib/Order/Minimal.lean
index cfc38ab8c1e32..688801c79c497 100644
--- a/Mathlib/Order/Minimal.lean
+++ b/Mathlib/Order/Minimal.lean
@@ -10,13 +10,8 @@ import Mathlib.Order.Interval.Set.Basic
 /-!
 # Minimality and Maximality
 
-This file defines minimality and maximality of an element with respect to a predicate `P` on
-an ordered type `α`.
-
-## Main declarations
-
-* `Minimal P x`: `x` is minimal satisfying `P`.
-* `Maximal P x`: `x` is maximal satisfying `P`.
+This file proves basic facts about minimality and maximality
+of an element with respect to a predicate `P` on an ordered type `α`.
 
 ## Implementation Details
 
@@ -52,24 +47,6 @@ section LE
 
 variable [LE α]
 
-/-- `Minimal P x` means that `x` is a minimal element satisfying `P`. -/
-def Minimal (P : α → Prop) (x : α) : Prop := P x ∧ ∀ ⦃y⦄, P y → y ≤ x → x ≤ y
-
-/-- `Maximal P x` means that `x` is a maximal element satisfying `P`. -/
-def Maximal (P : α → Prop) (x : α) : Prop := P x ∧ ∀ ⦃y⦄, P y → x ≤ y → y ≤ x
-
-lemma Minimal.prop (h : Minimal P x) : P x :=
-  h.1
-
-lemma Maximal.prop (h : Maximal P x) : P x :=
-  h.1
-
-lemma Minimal.le_of_le (h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y :=
-  h.2 hy hle
-
-lemma Maximal.le_of_ge (h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x :=
-  h.2 hy hge
-
 @[simp] theorem minimal_toDual : Minimal (fun x ↦ P (ofDual x)) (toDual x) ↔ Maximal P x :=
   Iff.rfl