rw in one or several instructions

Stream: general

[Rémy Degenne]

What are the most common reasons for the fact that sometimes rw a, rw b cannot be shortened to rw [a, b] ?

[Rémy Degenne]

and sorry for the vague question, I'll try coming up with a simple example

[Damiano Testa]

I am not entirely sure, but in my experience this happens when rw a solves a partial goal and you are left with a different goal to which rw b makes sense...

[Rémy Degenne]

and that is exactly the case in the code that caused my question. I have one goal, I do rw [a, b], rw c, where rw a causes a second goal to appear and rw b closes one. And I cannot do rw [a, b, c]. Thanks for the explanation.

[Damiano Testa]

No problem! Besides, I think that this is the first time that I have explained something in the Zulip chat: thanks for the opportunity!