feat: further tactic progress

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")

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,19 +279,27 @@ a✝ : n✝ = n✝
 :::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
 :::
 
@@ -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_
 :::