refactor(data/set/basic): Remove _eq lemmas (#16572)
This PR removes `_eq` lemmas from `data.set.basic` which asset a `rfl` propositional equality, in favour of the `iff` versions, and makes the latter `simp` lemmas if they weren't already.
Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
