rwa tactic behaviour doesn't match documentation

[Command-Master]

Description

The documentation of rwa says "rwa calls rw, then closes any remaining goals using assumption.", but in fact rwa is a macro of rw $rws:rwRuleSeq $[$loc:location]?; assumption, and it only calls assumption once, on the first goal.
Either the documentation should be corrected, or the tactic definition should be modified to use all_goals assumption - I don't know what's the intended behavior.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Good question. I would assume the goal (heh) is to solve all side goals, i.e. all newly created goals, with assumption? Which I think we discussed elsewhere could actually benefit from it's own composable syntax. But I digress.

How important is this rwa tactic even? Does it pull it's weight in terms of things people need to know about, things that need to be documented etc?

[nomeata]

Looked at some uses in mathlib and core. There are certainly many! One idiom is rwa [foo] at h, presumably with the assumption (heh) that assumption will use h to close the goal. I’m not very fond of this fast-and-loose tactic (the assumption will happily use other hypotheses, and then the proof goes through when maybe it shouldn't have). But given that it’s heavily used, we can just update the docstring to match reality and move on.