diff --git a/Manual/Meta/Tactics.lean b/Manual/Meta/Tactics.lean
index b2ea11a..3fe7936 100644
--- a/Manual/Meta/Tactics.lean
+++ b/Manual/Meta/Tactics.lean
@@ -35,7 +35,7 @@ def checkTacticExample (goal : Term) (proofPrefix : Syntax) (tactic : Syntax) (p
     synthesizeSyntheticMVars (postpone := .no)
   -- `runTactic` extraction done. Now prettyprint the proof state.
   let st1 := goalsToMessageData remainingGoals
-  logInfoAt proofPrefix st1
+  --logInfoAt proofPrefix st1
   let goodPre ← (← addMessageContext st1).toString
   if pre.getString != goodPre then
     logErrorAt pre m!"Mismatch. Expected {indentD goodPre}\n but got {indentD pre.getString}"
@@ -46,7 +46,7 @@ def checkTacticExample (goal : Term) (proofPrefix : Syntax) (tactic : Syntax) (p
       set (Tactic.State.mk remainingGoals)
       evalTactic tactic
   let st2 := goalsToMessageData remainingGoals'
-  logInfoAt tactic st2
+  --logInfoAt tactic st2
   let goodPost ← (← addMessageContext st2).toString
   if post.getString != goodPost then
     logErrorAt post m!"Mismatch. Expected {indentD goodPost}\n but got {indentD post.getString}"
@@ -76,7 +76,7 @@ def checkTacticExample'
 
   -- `runTactic` extraction done. Now prettyprint the proof state.
   let st1 := goalsToMessageData remainingGoals
-  logInfoAt proofPrefix st1
+  --logInfoAt proofPrefix st1
   let goodPre ← (← addMessageContext st1).toString
   if pre.getString.trim != goodPre.trim then
     Verso.Doc.Suggestion.saveSuggestion pre (goodPre.take 30 ++ "…") (goodPre ++ "\n")
@@ -97,7 +97,7 @@ def checkTacticExample'
       set (Tactic.State.mk remainingGoals)
       evalTactic tactic
   let st2 := goalsToMessageData remainingGoals'
-  logInfoAt tactic st2
+  --logInfoAt tactic st2
   let goodPost ← (← addMessageContext st2).toString
   if post.getString.trim != goodPost.trim then
     Verso.Doc.Suggestion.saveSuggestion post (goodPost.take 30 ++ "…") (goodPost ++ "\n")
diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean
index cbd67f9..fabd83f 100644
--- a/Manual/Tactics.lean
+++ b/Manual/Tactics.lean
@@ -52,9 +52,6 @@ Tactic proofs may be embedded via {keywordOf Lean.Parser.Term.byTactic}`by` in a
 
 ## Assumptions
 
-:::TODO
-Create a tactic documentation command that does what both of the following do, using the infrastructure from https://github.com/leanprover/lean4/pull/4490
-:::
 
 :::tactic Lean.Parser.Tactic.assumption
 :::
@@ -83,6 +80,9 @@ Create a tactic documentation command that does what both of the following do, u
 :::tactic "clear"
 :::
 
+:::tactic Lean.Parser.Tactic.applyAssumption
+:::
+
 ## Quantifiers
 
 :::TODO
@@ -193,6 +193,12 @@ a✝ : n✝ = n✝
 :::tactic "obtain"
 :::
 
+:::tactic "show"
+:::
+
+:::tactic Lean.Parser.Tactic.showTerm
+:::
+
 
 ### Goal Selection
 
@@ -229,12 +235,33 @@ a✝ : n✝ = n✝
 :::tactic Lean.Parser.Tactic.pushCast
 :::
 
+:::tactic Lean.Parser.Tactic.normCast0
+:::
+
+:::tactic Lean.Parser.Tactic.tacticNorm_cast_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticExact_mod_cast_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticApply_mod_cast_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticRw_mod_cast___
+:::
+
+:::tactic Lean.Parser.Tactic.tacticAssumption_mod_cast
+:::
+
 ## Relations
 
 :::tactic "rfl"
 :::
 
-:::tactic "rfl'"
+:::tactic Lean.Parser.Tactic.applyRfl
+:::
+
+:::tactic Lean.Parser.Tactic.tacticRfl
 :::
 
 :::tactic "symm"
@@ -252,12 +279,17 @@ a✝ : n✝ = n✝
 :::tactic "subst_eqs"
 :::
 
+:::tactic "subst_vars"
+:::
+
 :::tactic "congr"
 :::
 
 :::tactic "eq_refl"
 :::
 
+:::tactic "ac_rfl"
+:::
 
 ## Extensionality
 
@@ -265,6 +297,9 @@ a✝ : n✝ = n✝
 :::tactic "ext"
 :::
 
+:::tactic Lean.Elab.Tactic.Ext.tacticExt1___
+:::
+
 :::tactic Lean.Elab.Tactic.Ext.applyExtTheorem
 :::
 
@@ -285,6 +320,9 @@ a✝ : n✝ = n✝
 :::tactic "simp_arith"
 :::
 
+:::tactic Lean.Parser.Tactic.simpArithAutoUnfold
+:::
+
 :::tactic "dsimp"
 :::
 
@@ -334,6 +372,9 @@ a✝ : n✝ = n✝
 :::tactic "erw"
 :::
 
+:::tactic Lean.Parser.Tactic.tacticRwa__
+:::
+
 :::tactic "unfold"
 :::
 
@@ -491,6 +532,10 @@ a✝ : n✝ = n✝
 :::tactic Lean.Parser.Tactic.tacticLetI_
 :::
 
+:::tactic Lean.Parser.Tactic.tacticLet'_
+:::
+
+
 
 :::tactic "checkpoint"
 :::
@@ -543,11 +588,17 @@ These tactics are used during elaboration of terms to satisfy obligations that a
 :::tactic "array_get_dec"
 :::
 
+:::tactic tacticDecreasing_with_
+:::
+
 ## Conv
 
 :::tactic "conv"
 :::
 
+:::tactic Lean.Parser.Tactic.Conv.convTactic
+:::
+
 ## Debugging Utilities
 
 :::tactic "sorry"
@@ -559,11 +610,26 @@ These tactics are used during elaboration of terms to satisfy obligations that a
 :::tactic "dbg_trace"
 :::
 
+:::tactic Lean.Parser.Tactic.traceState
+:::
+
+:::tactic Lean.Parser.Tactic.traceMessage
+:::
+
 
 ## Other
 
 :::tactic "trivial"
 :::
 
+:::tactic "solve"
+:::
+
+:::tactic "solve_by_elim"
+:::
+
+
+:::tactic "infer_instance"
+:::
 :::tactic Lean.Parser.Tactic.tacticUnhygienic_
 :::
diff --git a/Manual/Tactics/Impls.lean b/Manual/Tactics/Impls.lean
new file mode 100644
index 0000000..a6344cd
--- /dev/null
+++ b/Manual/Tactics/Impls.lean
@@ -0,0 +1,209 @@
+import VersoManual
+
+import Lean.Parser.Term
+
+import Manual.Meta
+
+
+open Verso.Genre Manual
+
+open Lean.Elab.Tactic
+
+set_option pp.rawOnError true
+
+set_option linter.unusedVariables false
+
+#doc (Manual) "Tactic Implementations" =>
+
+:::TODO
+Delete this section, consider them implementation details
+:::
+
+These functions implement tactics.
+Because they parse tactic syntax directly, they are not particularly convenient to call from {name}`TacticM` code.
+
+{docstring Lean.Elab.Tactic.elabSetOption}
+
+{docstring Lean.Elab.Tactic.evalSeq1}
+
+{docstring Lean.Elab.Tactic.evalSimp}
+
+{docstring Lean.Elab.Tactic.evalSpecialize}
+
+{docstring Lean.Elab.Tactic.evalTacticAt}
+
+{docstring Lean.Elab.Tactic.evalSimpAll}
+
+{docstring Lean.Elab.Tactic.evalIntro.introStep}
+
+{docstring Lean.Elab.Tactic.evalDone}
+
+{docstring Lean.Elab.Tactic.evalRevert}
+
+{docstring Lean.Elab.Tactic.evalRight}
+
+{docstring Lean.Elab.Tactic.evalUnfold}
+
+{docstring Lean.Elab.Tactic.evalConstructor}
+
+{docstring Lean.Elab.Tactic.evalTacticCDot}
+
+{docstring Lean.Elab.Tactic.evalTraceMessage}
+
+{docstring Lean.Elab.Tactic.evalClear}
+
+{docstring Lean.Elab.Tactic.evalIntroMatch}
+
+{docstring Lean.Elab.Tactic.evalInduction}
+
+{docstring Lean.Elab.Tactic.evalApply}
+
+{docstring Lean.Elab.Tactic.evalUnknown}
+
+{docstring Lean.Elab.Tactic.evalRefl}
+
+{docstring Lean.Elab.Tactic.evalTactic.throwExs}
+
+{docstring Lean.Elab.Tactic.evalDSimp}
+
+{docstring Lean.Elab.Tactic.evalSepTactics.goEven}
+
+{docstring Lean.Elab.Tactic.evalAllGoals}
+
+{docstring Lean.Elab.Tactic.evalSplit}
+
+{docstring Lean.Elab.Tactic.evalInjection}
+
+{docstring Lean.Elab.Tactic.evalParen}
+
+{docstring Lean.Elab.Tactic.evalFocus}
+
+{docstring Lean.Elab.Tactic.evalLeft}
+
+{docstring Lean.Elab.Tactic.evalRotateRight}
+
+{docstring Lean.Elab.Tactic.evalWithReducible}
+
+{docstring Lean.Elab.Tactic.evalTactic.expandEval}
+
+{docstring Lean.Elab.Tactic.evalTraceState}
+
+{docstring Lean.Elab.Tactic.evalCase'}
+
+{docstring Lean.Elab.Tactic.evalSepTactics.goOdd}
+
+{docstring Lean.Elab.Tactic.evalWithReducibleAndInstances}
+
+{docstring Lean.Elab.Tactic.evalTacticSeqBracketed}
+
+{docstring Lean.Elab.Tactic.evalTactic.eval}
+
+{docstring Lean.Elab.Tactic.evalAlt}
+
+{docstring Lean.Elab.Tactic.evalGeneralize}
+
+{docstring Lean.Elab.Tactic.evalRewriteSeq}
+
+{docstring Lean.Elab.Tactic.evalSleep}
+
+{docstring Lean.Elab.Tactic.evalDSimpTrace}
+
+{docstring Lean.Elab.Tactic.evalReplace}
+
+{docstring Lean.Elab.Tactic.evalOpen}
+
+{docstring Lean.Elab.Tactic.evalAssumption}
+
+{docstring Lean.Elab.Tactic.evalSepTactics}
+
+{docstring Lean.Elab.Tactic.evalWithUnfoldingAll}
+
+{docstring Lean.Elab.Tactic.evalMatch}
+
+{docstring Lean.Elab.Tactic.evalRepeat1'}
+
+{docstring Lean.Elab.Tactic.evalFailIfSuccess}
+
+{docstring Lean.Elab.Tactic.evalRename}
+
+{docstring Lean.Elab.Tactic.evalFirst.loop}
+
+{docstring Lean.Elab.Tactic.evalSimpTrace}
+
+{docstring Lean.Elab.Tactic.evalFirst}
+
+{docstring Lean.Elab.Tactic.evalSubstVars}
+
+{docstring Lean.Elab.Tactic.evalRunTac}
+
+{docstring Lean.Elab.Tactic.evalSymmSaturate}
+
+{docstring Lean.Elab.Tactic.evalWithAnnotateState}
+
+{docstring Lean.Elab.Tactic.evalTacticAtRaw}
+
+{docstring Lean.Elab.Tactic.evalDbgTrace}
+
+{docstring Lean.Elab.Tactic.evalSubst}
+
+{docstring Lean.Elab.Tactic.evalNativeDecide}
+
+{docstring Lean.Elab.Tactic.evalCalc}
+
+{docstring Lean.Elab.Tactic.evalCase}
+
+{docstring Lean.Elab.Tactic.evalRepeat'}
+
+{docstring Lean.Elab.Tactic.evalRefine}
+
+{docstring Lean.Elab.Tactic.evalContradiction}
+
+{docstring Lean.Elab.Tactic.evalSymm}
+
+{docstring Lean.Elab.Tactic.evalInjections}
+
+{docstring Lean.Elab.Tactic.evalExact}
+
+{docstring Lean.Elab.Tactic.evalRotateLeft}
+
+{docstring Lean.Elab.Tactic.evalFail}
+
+{docstring Lean.Elab.Tactic.evalTactic}
+
+{docstring Lean.Elab.Tactic.evalSimpAllTrace}
+
+{docstring Lean.Elab.Tactic.evalRefine'}
+
+{docstring Lean.Elab.Tactic.evalChoice}
+
+{docstring Lean.Elab.Tactic.evalInduction.checkTargets}
+
+{docstring Lean.Elab.Tactic.evalIntro}
+
+{docstring Lean.Elab.Tactic.evalAnyGoals}
+
+{docstring Lean.Elab.Tactic.evalCases}
+
+{docstring Lean.Elab.Tactic.evalDelta}
+
+{docstring Lean.Elab.Tactic.evalDecide}
+
+{docstring Lean.Elab.Tactic.evalChoiceAux}
+
+{docstring Lean.Elab.Tactic.evalTacticSeq}
+
+{docstring Lean.Elab.Tactic.evalCheckpoint}
+
+{docstring Lean.Elab.Tactic.evalRenameInaccessibles}
+
+{docstring Lean.Elab.Tactic.evalIntros}
+
+{docstring Lean.Elab.Tactic.evalApplyLikeTactic}
+
+{docstring Lean.Elab.Tactic.evalSkip}
+
+{docstring Lean.Elab.Tactic.evalCalc.throwFailed}
+
+{docstring Lean.Elab.Tactic.evalSubstEqs}
+
+{docstring Lean.Elab.Tactic.evalTacticSeq1Indented}
diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean
new file mode 100644
index 0000000..f169e33
--- /dev/null
+++ b/Manual/Tactics/Reference.lean
@@ -0,0 +1,603 @@
+import VersoManual
+
+import Lean.Parser.Term
+
+import Manual.Meta
+
+
+open Verso.Genre Manual
+
+set_option pp.rawOnError true
+
+set_option linter.unusedVariables false
+
+#doc (Manual) "Reference" =>
+
+
+# Tactic Reference
+
+## Assumptions
+
+
+:::tactic Lean.Parser.Tactic.assumption
+:::
+
+:::tactic "rename"
+:::
+
+:::tactic "rename_i"
+:::
+
+:::tactic "have"
+:::
+
+:::tactic Lean.Parser.Tactic.«tacticHave'_:=_»
+:::
+
+:::tactic Lean.Parser.Tactic.tacticHaveI_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticHave'_
+:::
+
+:::tactic "revert"
+:::
+
+:::tactic "clear"
+:::
+
+:::tactic Lean.Parser.Tactic.applyAssumption
+:::
+
+## Quantifiers
+
+:::TODO
+Work around Markdown headers in `intro`, `intros` docs
+:::
+
+:::tactic Lean.Parser.Tactic.introMatch
+:::
+
+
+:::tactic "rintro"
+:::
+
+:::tactic "exists"
+:::
+
+
+Here is {tactic}`rintro` and Here is {tactic}`induction`
+
+:::tacticExample
+The goal is {goal}`∀(n : Nat), n = n`.
+```setup
+intro
+```
+After some tactics, it ends up being:
+```pre
+n✝ : Nat
+⊢ n✝ = n✝
+```
+Running {tacticStep}`skip` leaves
+```post
+n✝ : Nat
+⊢ n✝ = n✝
+```
+:::
+
+:::tacticExample
+The goal is {goal}`∀(n : Nat), n = n`.
+```setup
+intro n; induction n
+```
+After some tactics, it ends up being:
+```pre
+case zero
+⊢ 0 = 0
+
+case succ
+n✝ : Nat
+a✝ : n✝ = n✝
+⊢ n✝ + 1 = n✝ + 1
+```
+Running {tacticStep}`skip` leaves
+```post
+case zero
+⊢ 0 = 0
+
+case succ
+n✝ : Nat
+a✝ : n✝ = n✝
+⊢ n✝ + 1 = n✝ + 1
+```
+:::
+
+## Lemmas
+
+:::tactic "exact"
+:::
+
+:::tactic "apply"
+:::
+
+:::tactic "refine"
+:::
+
+:::tactic "refine'"
+:::
+
+
+## Falsehood
+
+:::tactic "exfalso"
+:::
+
+:::tactic "contradiction"
+:::
+
+:::tactic Lean.Parser.Tactic.falseOrByContra
+:::
+
+
+## Goal Management
+
+:::tactic "suffices"
+:::
+
+:::tactic "change"
+:::
+
+:::tactic Lean.Parser.Tactic.changeWith
+:::
+
+:::tactic "generalize"
+:::
+
+:::tactic "specialize"
+:::
+
+:::tactic "obtain"
+:::
+
+:::tactic "show"
+:::
+
+:::tactic Lean.Parser.Tactic.showTerm
+:::
+
+
+### Goal Selection
+
+:::tactic Lean.cdot
+:::
+
+:::tactic "case"
+:::
+
+:::tactic "case'"
+:::
+
+:::tactic "next"
+:::
+
+:::tactic "all_goals"
+:::
+
+:::tactic "any_goals"
+:::
+
+:::tactic "focus"
+:::
+
+:::tactic Lean.Parser.Tactic.rotateLeft
+:::
+
+:::tactic Lean.Parser.Tactic.rotateRight
+:::
+
+
+## Cast Management
+
+:::tactic Lean.Parser.Tactic.pushCast
+:::
+
+:::tactic Lean.Parser.Tactic.normCast0
+:::
+
+:::tactic Lean.Parser.Tactic.tacticNorm_cast_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticExact_mod_cast_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticApply_mod_cast_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticRw_mod_cast___
+:::
+
+:::tactic Lean.Parser.Tactic.tacticAssumption_mod_cast
+:::
+
+## Relations
+
+:::tactic "rfl"
+:::
+
+:::tactic Lean.Parser.Tactic.applyRfl
+:::
+
+:::tactic Lean.Parser.Tactic.tacticRfl
+:::
+
+:::tactic "symm"
+:::
+
+:::tactic "calc"
+:::
+
+
+### Equality
+
+:::tactic "subst"
+:::
+
+:::tactic "subst_eqs"
+:::
+
+:::tactic "subst_vars"
+:::
+
+:::tactic "congr"
+:::
+
+:::tactic "eq_refl"
+:::
+
+:::tactic "ac_rfl"
+:::
+
+## Extensionality
+
+
+:::tactic "ext"
+:::
+
+:::tactic Lean.Elab.Tactic.Ext.tacticExt1___
+:::
+
+:::tactic Lean.Elab.Tactic.Ext.applyExtTheorem
+:::
+
+:::tactic "funext"
+:::
+
+## Simplification
+
+:::tactic "simp"
+:::
+
+:::tactic "simp?"
+:::
+
+:::tactic "simp?!"
+:::
+
+:::tactic "simp_arith"
+:::
+
+:::tactic Lean.Parser.Tactic.simpArithAutoUnfold
+:::
+
+:::tactic "dsimp"
+:::
+
+:::tactic "dsimp?"
+:::
+
+:::tactic "dsimp?!"
+:::
+
+:::tactic "dsimp!"
+:::
+
+:::tactic "simp_all"
+:::
+
+:::tactic "simp_all?"
+:::
+
+:::tactic "simp_all?!"
+:::
+
+
+:::tactic "simp_all_arith"
+:::
+
+:::tactic "simpa"
+:::
+
+:::tactic "simpa?"
+:::
+
+:::tactic "simpa!"
+:::
+
+:::tactic "simpa?!"
+:::
+
+
+## Rewriting
+
+:::tactic "rw"
+:::
+
+:::tactic "rewrite"
+:::
+
+:::tactic "erw"
+:::
+
+:::tactic Lean.Parser.Tactic.tacticRwa__
+:::
+
+:::tactic "unfold"
+
+Implemented by {name}`Lean.Elab.Tactic.evalUnfold`.
+:::
+
+:::tactic "replace"
+:::
+
+:::tactic "delta"
+:::
+
+
+## Inductive Types
+
+:::tactic "constructor"
+:::
+
+:::tactic "cases"
+:::
+
+:::tactic "rcases"
+:::
+
+:::tactic "induction"
+:::
+
+:::tactic "injection"
+:::
+
+:::tactic "injections"
+:::
+
+:::tactic "left"
+:::
+
+:::tactic "right"
+:::
+
+
+## Library Search
+
+:::tactic "exact?"
+:::
+
+:::tactic "apply?"
+:::
+
+:::tactic "rw?"
+:::
+
+## Case Analysis
+
+:::tactic "split"
+:::
+
+:::tactic "by_cases"
+:::
+
+## Decision Procedures
+
+:::tactic "omega"
+:::
+
+:::TODO
+`decide`
+:::
+
+:::tactic Lean.Parser.Tactic.nativeDecide
+:::
+
+### SAT Solver Integration
+
+:::tactic "bv_omega"
+:::
+
+:::tactic "bv_decide"
+:::
+
+:::tactic "bv_normalize"
+:::
+
+:::tactic "bv_check"
+:::
+
+:::tactic Lean.Parser.Tactic.bvTrace
+:::
+
+## Control Flow
+
+:::tactic "skip"
+:::
+
+:::tactic "<;>"
+:::
+
+:::tactic "try"
+:::
+
+:::tactic "first"
+:::
+
+:::tactic Lean.Parser.Tactic.tacIfThenElse
+:::
+
+:::tactic Lean.Parser.Tactic.tacDepIfThenElse
+:::
+
+:::tactic Lean.Parser.Tactic.match
+:::
+
+:::tactic "nofun"
+:::
+
+:::tactic "nomatch"
+:::
+
+:::tactic "iterate"
+:::
+
+:::tactic "repeat"
+:::
+
+:::tactic "repeat'"
+:::
+
+:::tactic "repeat1'"
+:::
+
+
+:::tactic "fail"
+:::
+
+:::tactic "fail_if_success"
+:::
+
+:::tactic Lean.Parser.Tactic.guardHyp
+:::
+
+:::tactic Lean.Parser.Tactic.guardTarget
+:::
+
+:::tactic Lean.Parser.Tactic.guardExpr
+:::
+
+:::tactic "done"
+:::
+
+:::tactic "sleep"
+:::
+
+:::tactic "let"
+:::
+
+:::tactic Lean.Parser.Tactic.tacticLet_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticLetI_
+:::
+
+:::tactic Lean.Parser.Tactic.tacticLet'_
+:::
+
+
+
+:::tactic "checkpoint"
+:::
+
+:::tactic "save"
+:::
+
+:::tactic "stop"
+:::
+
+
+
+## Namespace and Option Management
+
+:::tactic Lean.Parser.Tactic.set_option
+:::
+
+:::tactic Lean.Parser.Tactic.open
+:::
+
+:::tactic Lean.Parser.Tactic.withReducibleAndInstances
+:::
+
+:::tactic Lean.Parser.Tactic.withReducible
+:::
+
+:::tactic Lean.Parser.Tactic.withUnfoldingAll
+:::
+
+
+## Term Elaboration Backends
+
+These tactics are used during elaboration of terms to satisfy obligations that arise.
+
+:::tactic "decreasing_tactic"
+:::
+
+:::tactic "decreasing_trivial"
+:::
+
+:::tactic "decreasing_trivial_pre_omega"
+:::
+
+:::tactic "get_elem_tactic"
+:::
+
+:::tactic "get_elem_tactic_trivial"
+:::
+
+:::tactic "array_get_dec"
+:::
+
+:::tactic tacticDecreasing_with_
+:::
+
+## Conv
+
+:::tactic "conv"
+:::
+
+:::tactic Lean.Parser.Tactic.Conv.convTactic
+:::
+
+## Debugging Utilities
+
+:::tactic "sorry"
+:::
+
+:::tactic "admit"
+:::
+
+:::tactic "dbg_trace"
+:::
+
+:::tactic Lean.Parser.Tactic.traceState
+:::
+
+:::tactic Lean.Parser.Tactic.traceMessage
+:::
+
+
+## Other
+
+:::tactic "trivial"
+:::
+
+:::tactic "solve"
+:::
+
+:::tactic "solve_by_elim"
+:::
+
+
+:::tactic "infer_instance"
+:::
+:::tactic Lean.Parser.Tactic.tacticUnhygienic_
+:::
diff --git a/lake-manifest.json b/lake-manifest.json
index 8206051..8822814 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2ddc0684c3f60b36e33c5f2ea541220a76b223f7",
+   "rev": "e7187854ccbf0a867a9c1ee3b25b4bd22460f812",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",