chore: minor tweaks to Sym.simp test and benchmark

This PR applies two minor tweaks:
- `tests/bench/sym/simp_1.lean`: share-common the proof term before
  counting objects in `getProofSize`, so the reported size reflects
  the shared representation.
- `tests/elab/sym_simp_3.lean`: use `>>` instead of `.andThen` when
  composing `Sym.Simp` methods.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

.github/workflows/ci.yml

@@ -279,8 +279,7 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                // Done as part of test-bench
-                //"check-stage3": level >= 2,
+                "check-stage3": level >= 2,
                 "test": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
@@ -292,8 +291,7 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                // Done as part of test-bench
-                //"check-stage3": level >= 2,
+                "check-stage3": level >= 2,
                 "test": true,
                 "secondary": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -329,19 +329,13 @@ def liftGoalM (k : GoalM α) : GrindTacticM α := do
   replaceMainGoal [goal]
   return a
 
-inductive LiftActionCoreResult where
-  | closed | subgoals
-
-def liftActionCore (a : Action) : GrindTacticM LiftActionCoreResult := do
+def liftAction (a : Action) : GrindTacticM Unit := do
   let goal ← getMainGoal
   let ka := fun _ => throwError "tactic is not applicable"
   let kp := fun goal => return .stuck [goal]
   match (← liftGrindM <| a goal ka kp) with
-  | .closed _ => replaceMainGoal []; return .closed
-  | .stuck gs => replaceMainGoal gs; return .subgoals
-
-def liftAction (a : Action) : GrindTacticM Unit := do
-  discard <| liftActionCore a
+  | .closed _ => replaceMainGoal []
+  | .stuck gs => replaceMainGoal gs
 
 def done : GrindTacticM Unit := do
   pruneSolvedGoals

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -111,9 +111,7 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
      This matches the behavior of these tactics in default tactic mode
      where `lia` can close `x > 1 → x + y + z > 0` directly. -/
   if (← read).sym then
-    match (← liftActionCore <| Action.intros 0 >> Action.assertAll) with
-    | .closed   => return () -- closed the goal
-    | .subgoals => pure () -- continue
+    liftAction <| Action.intros 0 >> Action.assertAll
   let recover := (← read).recover
   liftGoalM do
     let progress ← k

tests/bench/build/run_bench.sh

@@ -23,8 +23,6 @@ echo ">"
 echo "> Building $STAGE_NEXT..."
 echo ">"
 
-make -C "$BUILD_NEXT" clean-stdlib
-
 LAKE_OVERRIDE_LEAN=true LEAN="$(realpath fake_root/bin/lean)" \
 WRAPPER_PREFIX="$(realpath fake_root)" WRAPPER_OUT="$OUT" \
   lakeprof record -- \

tests/elab/sym_interactive_bugs.lean

@@ -1,16 +0,0 @@
-
-example (p q : Prop) : p → q → p ∧ q := by
-  sym =>
-    intro hp hq
-    apply And.intro
-    apply hp
-    apply hq
-
-register_sym_simp chainSimp where
-  post := ground >> rewrite [Nat.add_zero, Nat.zero_add]
-
-example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ y + (1 + 0) := by
-  sym =>
-    simp chainSimp
-    -- In the following tactic the goal is closed while preprocessing the target
-    lia