Merge pull request #83 from leanprover-community/minimise-imports

remove `import Mathlib.Tactic`
2025-02-01 23:00:02 +00:00
parent 301951e2ea d52e8bdc7d
commit cd8025d835
1 changed files with 3 additions and 1 deletions
--- 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