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.

Estimated changes