Step through rw

Stream: general

[Theo Sandstrom]

In the beginning stages of learning Lean, I find it helpful to step through proofs in Mathlib and understand each step. When I encounter a rw tactic, I can only see the state before and after applying all of the steps in the rw rule sequence. Is there a way to step through with more granularity? I have resorted to closing the square brackets early and commenting out the rest of the line, but this feels a bit hacky. I am using the emacs mode.

[Ruben Van de Velde]

In Vs code, you can put the cursor after each comma to see the intermediate state

[Derrik Petrin]

Is this the lean mode you are using: https://github.com/leanprover-community/lean4-mode ?
There's an older one that was for Lean 3. I use lean4-mode and can see incremental steps of a rw by moving the cursor along the list, like Ruben is describing for VS Code.