remove import Mathlib.Tactic

leanprover-community · Dec 19, 2024 · d52e8bd · d52e8bd
1 parent 66b27f3
commit d52e8bd
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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