From 33db591925254d7b3b50980b7dfd09565309f14a Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 4 Nov 2024 06:56:21 +0000
Subject: [PATCH] fix: TODO list

---
 scripts/find_TODOs.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/find_TODOs.lean b/scripts/find_TODOs.lean
index 1165c6b..6e8fbca 100644
--- a/scripts/find_TODOs.lean
+++ b/scripts/find_TODOs.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import Lean
 import Batteries.Data.String.Matcher
-import Mathlib.Init.Data.Nat.Lemmas
+import Mathlib.Data.Nat.Notation
 /-!
 
 # TODO finder