fix import

leanprover-community · May 3, 2024 · bd9d0c3 · bd9d0c3
1 parent f09da0a
commit bd9d0c3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
@@ -5,7 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Std.Control.ForInStep.Lemmas
 import Std.Data.List.Basic
-import Std.Data.Nat
+import Std.Data.Nat.Lemmas
 import Std.Tactic.Init
 import Std.Tactic.Alias