Commit 2022-09-22 18:41 951bf1d9
View on Github →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.