Commit 2022-12-13 10:52 eb136dd2
View on Github →feat: Data.Set.Basic Add mem_setOf_eq (#962)
Adding a missing lemma from Lean3 core. Alternatively we could just mark mem_setOf
as a simp
lemma and align Lean3's set.mem_set_of_eq
, but the statements are slightly different Eq
versus Iff
so this is probably the method that make porting the easiest.