chore(data/set/basic): add set.subsingleton.pairwise_on (#7257)

Also add `set.pairwise_on_singleton`.

src/data/set/basic.lean

@@ -1789,9 +1789,17 @@ begin
     rw [hz x hx, hz y hy] }
 end
 
-@[simp] lemma pairwise_on_empty {α} (r : α → α → Prop) :
+protected lemma subsingleton.pairwise_on (h : s.subsingleton) (r : α → α → Prop) :
+  pairwise_on s r :=
+λ x hx y hy hne, (hne (h hx hy)).elim
+
+@[simp] lemma pairwise_on_empty (r : α → α → Prop) :
   (∅ : set α).pairwise_on r :=
-λ _, by simp
+subsingleton_empty.pairwise_on r
+
+@[simp] lemma pairwise_on_singleton (a : α) (r : α → α → Prop) :
+  pairwise_on {a} r :=
+subsingleton_singleton.pairwise_on r
 
 lemma pairwise_on_insert_of_symmetric {α} {s : set α} {a : α} {r : α → α → Prop}
   (hr : symmetric r) :