linter.fugue.rwaExact

rw [...] at h then exact h, or rw [...] then exact h for a hypothesis already in context, is rwa — the rewrite absorbs the closing assumption. Same for erw / erwa.

This linter covers the at h form (the name is right there in the rewrite). The bare rw […]; exact <hyp> form needs an is-local check — linter.fugue.rwaExactBare (Sem).