do not import all of mathlib

Game/Metadata.lean

@@ -5,7 +5,7 @@ import Game.MyNat.Definition
 import Game.Doc.Definitions
 import Game.Doc.Tactics
 
-import Mathlib.Tactic
+import Game.Tactic.FromMathlib
 
 import Game.Tactic.Induction
 import Game.Tactic.Cases

Game/MyNat/DecidableEq.lean

@@ -1,6 +1,6 @@
 import Game.MyNat.PeanoAxioms
 import Game.Levels.Algorithm.L07succ_ne_succ -- succ_ne_succ
-import Game.Tactic.decide -- modified decide tactic
+import Game.Tactic.Decide -- modified decide tactic
 
 namespace MyNat
 

Game/Tactic/FromMathlib.lean

@@ -0,0 +1,204 @@
+import Mathlib.Tactic.NthRewrite
+import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.Ring -- this is bad because it adds `mul_comm` to the `_root_` namespace, interfering with `MyNat.mul_comm`.
+
+
+-- import Mathlib.Tactic.Abel
+-- import Mathlib.Tactic.ApplyAt
+-- import Mathlib.Tactic.ApplyCongr
+-- import Mathlib.Tactic.ApplyFun
+-- import Mathlib.Tactic.ApplyWith
+-- import Mathlib.Tactic.ArithMult
+-- import Mathlib.Tactic.ArithMult.Init
+-- import Mathlib.Tactic.Attr.Core
+-- import Mathlib.Tactic.Attr.Register
+-- import Mathlib.Tactic.Basic
+-- import Mathlib.Tactic.ByContra
+-- import Mathlib.Tactic.CancelDenoms
+-- import Mathlib.Tactic.CancelDenoms.Core
+-- import Mathlib.Tactic.Cases
+-- import Mathlib.Tactic.CasesM
+-- import Mathlib.Tactic.CategoryTheory.BicategoryCoherence
+-- import Mathlib.Tactic.CategoryTheory.Coherence
+-- import Mathlib.Tactic.CategoryTheory.Elementwise
+-- import Mathlib.Tactic.CategoryTheory.Reassoc
+-- import Mathlib.Tactic.CategoryTheory.Slice
+-- import Mathlib.Tactic.Change
+-- import Mathlib.Tactic.Check
+-- import Mathlib.Tactic.Choose
+-- import Mathlib.Tactic.Clean
+-- import Mathlib.Tactic.Clear!
+-- import Mathlib.Tactic.ClearExcept
+-- import Mathlib.Tactic.Clear_
+-- import Mathlib.Tactic.Coe
+-- import Mathlib.Tactic.Common
+-- import Mathlib.Tactic.ComputeDegree
+-- import Mathlib.Tactic.Congr!
+-- import Mathlib.Tactic.Congrm
+-- import Mathlib.Tactic.Constructor
+-- import Mathlib.Tactic.Continuity
+-- import Mathlib.Tactic.Continuity.Init
+-- import Mathlib.Tactic.Contrapose
+-- import Mathlib.Tactic.Conv
+-- import Mathlib.Tactic.Convert
+-- import Mathlib.Tactic.Core
+-- import Mathlib.Tactic.DefEqTransformations
+-- import Mathlib.Tactic.DeriveFintype
+-- import Mathlib.Tactic.DeriveToExpr
+-- import Mathlib.Tactic.DeriveTraversable
+-- import Mathlib.Tactic.Eqns
+-- import Mathlib.Tactic.Existsi
+-- import Mathlib.Tactic.Explode
+-- import Mathlib.Tactic.Explode.Datatypes
+-- import Mathlib.Tactic.Explode.Pretty
+-- import Mathlib.Tactic.ExtendDoc
+-- import Mathlib.Tactic.ExtractGoal
+-- import Mathlib.Tactic.ExtractLets
+-- import Mathlib.Tactic.FBinop
+-- import Mathlib.Tactic.FailIfNoProgress
+-- import Mathlib.Tactic.FieldSimp
+-- import Mathlib.Tactic.FinCases
+-- import Mathlib.Tactic.Find
+-- import Mathlib.Tactic.FunProp
+-- import Mathlib.Tactic.FunProp.AEMeasurable
+-- import Mathlib.Tactic.FunProp.Attr
+-- import Mathlib.Tactic.FunProp.ContDiff
+-- import Mathlib.Tactic.FunProp.Core
+-- import Mathlib.Tactic.FunProp.Decl
+-- import Mathlib.Tactic.FunProp.Differentiable
+-- import Mathlib.Tactic.FunProp.Elab
+-- import Mathlib.Tactic.FunProp.FunctionData
+-- import Mathlib.Tactic.FunProp.Measurable
+-- import Mathlib.Tactic.FunProp.Mor
+-- import Mathlib.Tactic.FunProp.RefinedDiscrTree
+-- import Mathlib.Tactic.FunProp.StateList
+-- import Mathlib.Tactic.FunProp.Theorems
+-- import Mathlib.Tactic.FunProp.ToStd
+-- import Mathlib.Tactic.FunProp.Types
+-- import Mathlib.Tactic.GCongr
+-- import Mathlib.Tactic.GCongr.Core
+-- import Mathlib.Tactic.GCongr.ForwardAttr
+-- import Mathlib.Tactic.GeneralizeProofs
+-- import Mathlib.Tactic.Group
+-- import Mathlib.Tactic.GuardGoalNums
+-- import Mathlib.Tactic.GuardHypNums
+-- import Mathlib.Tactic.Have
+-- import Mathlib.Tactic.HaveI
+-- import Mathlib.Tactic.HelpCmd
+-- import Mathlib.Tactic.HigherOrder
+-- import Mathlib.Tactic.Hint
+-- import Mathlib.Tactic.InferParam
+-- import Mathlib.Tactic.Inhabit
+-- import Mathlib.Tactic.IntervalCases
+-- import Mathlib.Tactic.IrreducibleDef
+-- import Mathlib.Tactic.Lemma
+-- import Mathlib.Tactic.LibrarySearch
+-- import Mathlib.Tactic.Lift
+-- import Mathlib.Tactic.LiftLets
+-- import Mathlib.Tactic.Linarith
+-- import Mathlib.Tactic.Linarith.Datatypes
+-- import Mathlib.Tactic.Linarith.Elimination
+-- import Mathlib.Tactic.Linarith.Frontend
+-- import Mathlib.Tactic.Linarith.Lemmas
+-- import Mathlib.Tactic.Linarith.Parsing
+-- import Mathlib.Tactic.Linarith.Preprocessing
+-- import Mathlib.Tactic.Linarith.Verification
+-- import Mathlib.Tactic.LinearCombination
+-- import Mathlib.Tactic.Lint
+-- import Mathlib.Tactic.Measurability
+-- import Mathlib.Tactic.Measurability.Init
+-- import Mathlib.Tactic.MkIffOfInductiveProp
+-- import Mathlib.Tactic.ModCases
+-- import Mathlib.Tactic.Monotonicity
+-- import Mathlib.Tactic.Monotonicity.Attr
+-- import Mathlib.Tactic.Monotonicity.Basic
+-- import Mathlib.Tactic.Monotonicity.Lemmas
+-- import Mathlib.Tactic.MoveAdd
+-- import Mathlib.Tactic.NoncommRing
+-- import Mathlib.Tactic.Nontriviality
+-- import Mathlib.Tactic.Nontriviality.Core
+-- import Mathlib.Tactic.NormNum
+-- import Mathlib.Tactic.NormNum.Basic
+-- import Mathlib.Tactic.NormNum.BigOperators
+-- import Mathlib.Tactic.NormNum.Core
+-- import Mathlib.Tactic.NormNum.DivMod
+-- import Mathlib.Tactic.NormNum.Eq
+-- import Mathlib.Tactic.NormNum.GCD
+-- import Mathlib.Tactic.NormNum.Ineq
+-- import Mathlib.Tactic.NormNum.Inv
+-- import Mathlib.Tactic.NormNum.IsCoprime
+-- import Mathlib.Tactic.NormNum.LegendreSymbol
+-- import Mathlib.Tactic.NormNum.NatFib
+-- import Mathlib.Tactic.NormNum.NatSqrt
+-- import Mathlib.Tactic.NormNum.OfScientific
+-- import Mathlib.Tactic.NormNum.Pow
+-- import Mathlib.Tactic.NormNum.Prime
+-- import Mathlib.Tactic.NormNum.Result
+-- import Mathlib.Tactic.Observe
+-- import Mathlib.Tactic.PPWithUniv
+-- import Mathlib.Tactic.Peel
+-- import Mathlib.Tactic.Polyrith
+-- import Mathlib.Tactic.Positivity
+-- import Mathlib.Tactic.Positivity.Basic
+-- import Mathlib.Tactic.Positivity.Core
+-- import Mathlib.Tactic.ProdAssoc
+-- import Mathlib.Tactic.ProjectionNotation
+-- import Mathlib.Tactic.Propose
+-- import Mathlib.Tactic.ProxyType
+-- import Mathlib.Tactic.PushNeg
+-- import Mathlib.Tactic.Qify
+-- import Mathlib.Tactic.RSuffices
+-- import Mathlib.Tactic.Recall
+-- import Mathlib.Tactic.Recover
+-- import Mathlib.Tactic.ReduceModChar
+-- import Mathlib.Tactic.ReduceModChar.Ext
+-- import Mathlib.Tactic.Relation.Rfl
+-- import Mathlib.Tactic.Relation.Symm
+-- import Mathlib.Tactic.Relation.Trans
+-- import Mathlib.Tactic.Rename
+-- import Mathlib.Tactic.RenameBVar
+-- import Mathlib.Tactic.Replace
+-- import Mathlib.Tactic.RewriteSearch
+-- import Mathlib.Tactic.Rewrites
+-- import Mathlib.Tactic.Rify
+-- import Mathlib.Tactic.Ring.Basic
+-- import Mathlib.Tactic.Ring.PNat
+-- import Mathlib.Tactic.Ring.RingNF
+-- import Mathlib.Tactic.RunCmd
+-- import Mathlib.Tactic.Sat.FromLRAT
+-- import Mathlib.Tactic.Says
+-- import Mathlib.Tactic.ScopedNS
+-- import Mathlib.Tactic.Set
+-- import Mathlib.Tactic.SetLike
+-- import Mathlib.Tactic.SimpIntro
+-- import Mathlib.Tactic.SimpRw
+-- import Mathlib.Tactic.Simps.Basic
+-- import Mathlib.Tactic.Simps.NotationClass
+-- import Mathlib.Tactic.SlimCheck
+-- import Mathlib.Tactic.SplitIfs
+-- import Mathlib.Tactic.Spread
+-- import Mathlib.Tactic.Substs
+-- import Mathlib.Tactic.SuccessIfFailWithMsg
+-- import Mathlib.Tactic.SudoSetOption
+-- import Mathlib.Tactic.SuppressCompilation
+-- import Mathlib.Tactic.SwapVar
+-- import Mathlib.Tactic.TFAE
+-- import Mathlib.Tactic.TermCongr
+-- import Mathlib.Tactic.ToAdditive
+-- import Mathlib.Tactic.ToExpr
+-- import Mathlib.Tactic.ToLevel
+-- import Mathlib.Tactic.Trace
+-- import Mathlib.Tactic.TypeCheck
+-- import Mathlib.Tactic.TypeStar
+-- import Mathlib.Tactic.UnsetOption
+-- import Mathlib.Tactic.Use
+-- import Mathlib.Tactic.Variable
+-- import Mathlib.Tactic.WLOG
+-- import Mathlib.Tactic.Widget.Calc
+-- import Mathlib.Tactic.Widget.CommDiag
+-- import Mathlib.Tactic.Widget.Congrm
+-- import Mathlib.Tactic.Widget.Conv
+-- import Mathlib.Tactic.Widget.Gcongr
+-- import Mathlib.Tactic.Widget.SelectInsertParamsClass
+-- import Mathlib.Tactic.Widget.SelectPanelUtils
+-- import Mathlib.Tactic.Zify