theorem Set.mem_sep
theorem Set.mem_sep: ∀ {α : Type u} {s : Set α} {x : α} {p : α → Prop}, x ∈ s → p x → x ∈ setOf fun x => x ∈ s ∧ p x
theorem Set.mem_sep
theorem Set.mem_sep: ∀ {α : Type u} {s : Set α} {x : α} {p : α → Prop}, x ∈ s → p x → x ∈ setOf fun x => x ∈ s ∧ p x