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

remove `import Mathlib.Tactic`
leanprover-community · Feb 1, 2025 · cd8025d · cd8025d
2 parents 301951e + d52e8bd
commit cd8025d
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