feat: Pairwise.range_pairwise (#10957)

Add another lemma relating `_root_.Pairwise` and `Set.Pairwise`:

```lean
lemma Pairwise.range_pairwise (hr : Pairwise (r on f)) : (Set.range f).Pairwise r := by
```

From AperiodicMonotilesLean.




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Set/Pairwise/Basic.lean

@@ -224,6 +224,9 @@ theorem InjOn.pairwise_image {s : Set ι} (h : s.InjOn f) :
   simp (config := { contextual := true }) [h.eq_iff, Set.Pairwise]
 #align set.inj_on.pairwise_image Set.InjOn.pairwise_image
 
+lemma _root_.Pairwise.range_pairwise (hr : Pairwise (r on f)) : (Set.range f).Pairwise r :=
+  image_univ ▸ (pairwise_univ.mpr hr).image
+
 end Set
 
 end Pairwise
@@ -355,9 +358,8 @@ end SemilatticeInfBot
 variable {s : Set ι} {t : Set ι'}
 
 theorem pairwiseDisjoint_range_singleton :
-    (range (singleton : ι → Set ι)).PairwiseDisjoint id := by
-  rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
-  exact disjoint_singleton.2 (ne_of_apply_ne _ h)
+    (range (singleton : ι → Set ι)).PairwiseDisjoint id :=
+  Pairwise.range_pairwise fun _ _ => disjoint_singleton.2
 #align set.pairwise_disjoint_range_singleton Set.pairwiseDisjoint_range_singleton
 
 theorem pairwiseDisjoint_fiber (f : ι → α) (s : Set α) : s.PairwiseDisjoint fun a => f ⁻¹' {a} :=