diff --git a/tests/lean/626b.hlean b/tests/lean/626b.hlean
index 993e4c37b..4ab5956ae 100644
--- a/tests/lean/626b.hlean
+++ b/tests/lean/626b.hlean
@@ -1,4 +1,4 @@
-import hit.circle
+import homotopy.circle
 open circle
 
 definition f (x : S¹) : bool := circle.rec_on x _ _
diff --git a/tests/lean/hott/614.hlean b/tests/lean/hott/614.hlean
index bd3521479..075fb966a 100644
--- a/tests/lean/hott/614.hlean
+++ b/tests/lean/hott/614.hlean
@@ -1,4 +1,4 @@
-import hit.circle
+import homotopy.circle
 
 open circle eq int pi
 
diff --git a/tests/lean/hott/615.hlean b/tests/lean/hott/615.hlean
index 74c5d0c1a..021003ab5 100644
--- a/tests/lean/hott/615.hlean
+++ b/tests/lean/hott/615.hlean
@@ -1,5 +1,5 @@
 -- HoTT
-import hit.circle
+import homotopy.circle
 open circle eq int pi
 
 attribute circle.rec circle.elim [recursor 4]
diff --git a/tests/lean/hott/ind_tac4.hlean b/tests/lean/hott/ind_tac4.hlean
index b35a6f49d..55c33a007 100644
--- a/tests/lean/hott/ind_tac4.hlean
+++ b/tests/lean/hott/ind_tac4.hlean
@@ -1,4 +1,4 @@
-import hit.circle
+import homotopy.circle
 open circle
 
 attribute circle.elim_on [recursor 2]