theorem Set.mem_of_mem_inter_left
theorem Set.mem_of_mem_inter_left: ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a ∩ b → x ∈ a
theorem Set.mem_of_mem_inter_left
theorem Set.mem_of_mem_inter_left: ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a ∩ b → x ∈ a