remove import Mathlib.Tactic from LE file

leanprover-community · Nov 12, 2023 · 1f8cebd · 1f8cebd
1 parent dff90d7
commit 1f8cebd
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Game/MyNat/LE.lean b/Game/MyNat/LE.lean
@@ -1,5 +1,5 @@
 import Game.MyNat.Multiplication
-import Mathlib.Tactic
+--import Mathlib.Tactic
 
 namespace MyNat