Commit 2025-09-11 00:51 9fe66587

fix(TacticAnalysis): include more CommandElabM state calling runTactic (#29505) This PR fixes a few "unknown universe v" errors when running the tactic analysis framework on Mathlib. We need to move more state from the CommandElabM to the TermElabM that ends up running tactic code. Since we do essentially the same in a few places, bundle up all the state manipulation into a new function runTacticCode.