diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 51396dacc0..6ee14b499b 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/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 =>
diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean
index d457f98b35..886fadf7f9 100644
--- a/tests/lean/run/allGoals.lean
+++ b/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