From f33eb309e19aaf254883837626526c4848c1c07d Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Sun, 12 Nov 2023 12:30:06 +0000
Subject: [PATCH] remove excessive import

---
 Game/MyNat/DecidableEq.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
index 3f9e300..6257dab 100644
--- a/Game/MyNat/DecidableEq.lean
+++ b/Game/MyNat/DecidableEq.lean
@@ -1,7 +1,6 @@
 import Game.MyNat.PeanoAxioms
 import Game.Levels.Algorithm.L07succ_ne_succ -- succ_ne_succ
-import Mathlib.Tactic
-import Game.Tactic.decide
+import Game.Tactic.decide -- modified decide tactic
 
 namespace MyNat