diff --git a/.i18n/Game.pot b/.i18n/Game.pot
index ac49b2f..c2294ab 100644
--- a/.i18n/Game.pot
+++ b/.i18n/Game.pot
@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.6.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Mon Mar 11 19:40:35 2024\n"
+"POT-Creation-Date: Thu Mar 14 10:26:53 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
diff --git a/Game/Metadata.lean b/Game/Metadata.lean
index 79d70c8..85cb142 100644
--- a/Game/Metadata.lean
+++ b/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
diff --git a/Game/Tactic/FromMathlib.lean b/Game/Tactic/FromMathlib.lean
new file mode 100644
index 0000000..e41bad7
--- /dev/null
+++ b/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
diff --git a/Game/Tactic/Xyzzy.lean b/Game/Tactic/Xyzzy.lean
index 927c343..01f0d49 100644
--- a/Game/Tactic/Xyzzy.lean
+++ b/Game/Tactic/Xyzzy.lean
@@ -3,11 +3,11 @@ import Lean
 universe u
 
 @[never_extract]
-axiom iGiveUpAx (α : Sort u) (synthetic := false) : α
+axiom xyzzyAxiom (α : Sort u) (synthetic := false) : α
 
 /--
 `xyzzy` is an ancient magic word, believed to be the root of the
 modern word `sorry`. The game won't complain - or notice - if you
 prove anything with `xyzzy`.
 -/
-macro "xyzzy" : tactic => `(tactic| exact @iGiveUpAx _ false)
+macro "xyzzy" : tactic => `(tactic| exact @xyzzyAxiom _ false)
diff --git a/lake-manifest.json b/lake-manifest.json
index dde70c6..e1af1c3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -19,14 +19,11 @@
    "inputRev": "v4.6.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/lean4game.git",
-   "type": "git",
-   "subDir": "server",
-   "rev": "68f84a3426684914f834342854bf4963ba2d8d57",
+  {"type": "path",
    "name": "GameServer",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
    "inherited": false,
+   "dir": "./../lean4game/server",
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",