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