diff --git a/Mathlib.lean b/Mathlib.lean
index 1ba09380d0850d..244c21393138f2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6283,10 +6283,10 @@ public import Mathlib.Order.CompleteLattice.Group
 public import Mathlib.Order.CompleteLattice.Lemmas
 public import Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
 public import Mathlib.Order.CompleteLattice.PiLex
-public import Mathlib.Order.CompleteLattice.SetLike
 public import Mathlib.Order.CompleteLatticeIntervals
 public import Mathlib.Order.CompletePartialOrder
-public import Mathlib.Order.CompleteSublattice
+public import Mathlib.Order.CompleteSublattice.Basic
+public import Mathlib.Order.CompleteSublattice.SetLike
 public import Mathlib.Order.Completion
 public import Mathlib.Order.Concept
 public import Mathlib.Order.ConditionallyCompleteLattice.Basic
diff --git a/Mathlib/Order/CompleteSublattice.lean b/Mathlib/Order/CompleteSublattice/Basic.lean
similarity index 100%
rename from Mathlib/Order/CompleteSublattice.lean
rename to Mathlib/Order/CompleteSublattice/Basic.lean
diff --git a/Mathlib/Order/CompleteLattice/SetLike.lean b/Mathlib/Order/CompleteSublattice/SetLike.lean
similarity index 97%
rename from Mathlib/Order/CompleteLattice/SetLike.lean
rename to Mathlib/Order/CompleteSublattice/SetLike.lean
index 8b582cdc3ed6cc..d381a0c708539f 100644
--- a/Mathlib/Order/CompleteLattice/SetLike.lean
+++ b/Mathlib/Order/CompleteSublattice/SetLike.lean
@@ -5,7 +5,7 @@ Authors: Sven Manthe
 -/
 module
 
-public import Mathlib.Order.CompleteSublattice
+public import Mathlib.Order.CompleteSublattice.Basic
 
 set_option doc.verso true
 set_option doc.verso.suggestions false
diff --git a/Mathlib/RingTheory/SimpleModule/Isotypic.lean b/Mathlib/RingTheory/SimpleModule/Isotypic.lean
index 2fa7a340861317..e95f98c30fe6a7 100644
--- a/Mathlib/RingTheory/SimpleModule/Isotypic.lean
+++ b/Mathlib/RingTheory/SimpleModule/Isotypic.lean
@@ -6,7 +6,7 @@ Authors: Junyan Xu
 module
 
 public import Mathlib.Algebra.Algebra.Pi
-public import Mathlib.Order.CompleteSublattice
+public import Mathlib.Order.CompleteSublattice.Basic
 public import Mathlib.RingTheory.SimpleModule.Basic
 
 /-!
diff --git a/Mathlib/SetTheory/Descriptive/Tree.lean b/Mathlib/SetTheory/Descriptive/Tree.lean
index d0de8f41bddfc3..58e8d4a3716af1 100644
--- a/Mathlib/SetTheory/Descriptive/Tree.lean
+++ b/Mathlib/SetTheory/Descriptive/Tree.lean
@@ -5,7 +5,7 @@ Authors: Sven Manthe
 -/
 module
 
-public import Mathlib.Order.CompleteLattice.SetLike
+public import Mathlib.Order.CompleteSublattice.SetLike
 
 set_option doc.verso true
 set_option doc.verso.suggestions false