There is nowhere that I can put my cursor to see the state between the two rewrites ```lean4 example {x : ℕ} : 1 + x * 2 = x + x + 1 := by simp_rw [mul_two, add_comm] ``` This was possible in Lean 3. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Stepping.20through.20simp_rw/near/326712986)
There is nowhere that I can put my cursor to see the state between the two rewrites
This was possible in Lean 3.
Zulip thread