linter.fugue.rwBeforeSimp

A rw […] immediately before a simp only […] / grind is two traversals where one would do, and rw's closing rfl attempt is dead work when a simp/grind follows. Fold the lemmas into the simp only set, or — where that overshoots — use rewrite.