From 1f8cebdca9ccbc42024bee1b0b730d482369a7b5 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sun, 12 Nov 2023 12:44:18 +0000
Subject: [PATCH] remove `import Mathlib.Tactic` from LE file

---
 Game/MyNat/LE.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Game/MyNat/LE.lean b/Game/MyNat/LE.lean
index 1917e33..c741c50 100644
--- 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