theorem Set.mem_pair {α : Type u_1} {a b x : α} : x ∈ {a, b} ↔ x = a ∨ x = b

theorem Set.mem_image_fst_of_mem {α : Type u_1} {β : Type u_2} {x : α} (y : β) {S : Set (α × β)} (h : (x, y) ∈ S) : x ∈ Prod.fst '' S

theorem Set.mem_image_snd_of_mem {α : Type u_1} {β : Type u_2} {x : α} (y : β) {S : Set (α × β)} (h : (x, y) ∈ S) : y ∈ Prod.snd '' S

theorem Set.exists_mem_of_mem_image_fst {α : Type u_1} {β : Type u_2} {x : α} {S : Set (α × β)} (h : x ∈ Prod.fst '' S) : ∃ (y : β), (x, y) ∈ S

theorem Set.exists_mem_of_mem_image_snd {α : Type u_1} {β : Type u_2} {y : β} {S : Set (α × β)} (h : y ∈ Prod.snd '' S) : ∃ (x : α), (x, y) ∈ S