From d52e8bdc7d159ffa83e9a86f4d1672f9056e0997 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Thu, 19 Dec 2024 19:41:23 +0000
Subject: [PATCH] remove `import Mathlib.Tactic`

---
 Game/MyNat/PeanoAxioms.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Game/MyNat/PeanoAxioms.lean b/Game/MyNat/PeanoAxioms.lean
index a96a9a4..0e0ddee 100644
--- a/Game/MyNat/PeanoAxioms.lean
+++ b/Game/MyNat/PeanoAxioms.lean
@@ -1,5 +1,7 @@
 import Game.MyNat.Definition
-import Mathlib.Tactic
+import Mathlib.Tactic.ApplyAt
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Have
 
 namespace MyNat