linter.fugue.rwaExactBare

rw [S] (no at) immediately followed by exact h for a hypothesis h already in context is rwa [S] — the rewrite absorbs the closing assumption. Same for erw / simp_rw.

The rw [S] at h form is linter.fugue.rwaExact (Syn): there the name in the rewrite already says h is a hypothesis. In the bare form the identifier could be a global lemma — and rwa (rw then assumption) closes the goal only from a local hypothesis — so this linter reads the InfoTree and flags only when h names a local declaration of the goal the exact faced.