feat(Data/Set/Pairwise/Basic): pairwise disjoint sets and subsingleto…

…ns (#11629)

Add a lemma giving a characterization of pairwise disjoint sets in terms of each value lying in at most one set:

```lean
lemma subsingleton_setOf_mem_iff_pairwise_disjoint {f : ι → Set α} :
    (∀ a, {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Disjoint on f) :=
```

From AperiodicMonotilesLean.

Mathlib/Data/Set/Pairwise/Basic.lean

@@ -458,3 +458,8 @@ lemma exists_lt_mem_inter_of_not_pairwise_disjoint [LinearOrder ι]
 theorem pairwise_disjoint_fiber (f : ι → α) : Pairwise (Disjoint on fun a : α => f ⁻¹' {a}) :=
   pairwise_univ.1 <| Set.pairwiseDisjoint_fiber f univ
 #align pairwise_disjoint_fiber pairwise_disjoint_fiber
+
+lemma subsingleton_setOf_mem_iff_pairwise_disjoint {f : ι → Set α} :
+    (∀ a, {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Disjoint on f) :=
+  ⟨fun h _ _ hij ↦ disjoint_left.2 fun a hi hj ↦ hij (h a hi hj),
+   fun h _ _ hx _ hy ↦ by_contra fun hne ↦ disjoint_left.1 (h hne) hx hy⟩