Commit 2022-12-14 16:48 4f850b67

feat: port Data.SetLike.Basic (#993) mathlib3 SHA: fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e porting notes:

on SetLike.exists and SetLike.forall, the statement had to be massaged from ∃ x ∈ p, q ⟨x, ‹_›⟩ to ∃ (x : B) (h : x ∈ p), q ⟨x, ‹_›⟩. Is this a bug? Answer: No, this is because ∃ x ∈ p is now sugar for ∃ x, x ∈ p ∧ ... instead of ∃ x, ∃ (h : x ∈ p), ...
some lemmas were tagged with @[mono] but we don't have this attribute yet. I removed them but left porting notes with "TODO" to add them back.