fix: bug at allGoals

src/Lean/Elab/Tactic/Basic.lean

@@ -341,9 +341,10 @@ private def getOptRotation (stx : Syntax) : Nat :=
   let gs ← getUnsolvedGoals
   let mut gsNew := []
   for g in gs do
-    setGoals [g]
-    evalTactic stx[1]
-    gsNew := gsNew ++ (← getUnsolvedGoals)
+    unless ← isExprMVarAssigned g do
+      setGoals [g]
+      evalTactic stx[1]
+      gsNew := gsNew ++ (← getUnsolvedGoals)
   setGoals gsNew
 
 @[builtinTactic tacticSeq] def evalTacticSeq : Tactic := fun stx =>

tests/lean/run/allGoals.lean

@@ -58,3 +58,6 @@ theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by
   cases d <;> rw idEq
   traceState
   allGoals rfl
+
+def bug {a b c : Nat} (h₁ : a = b) (h₂ : b = c) : a = c := by
+  apply Eq.trans <;> assumption