feat: funext_iff_of_subsingleton (#11140)

Add a lemma about equality of functions from a subsingleton type:

```lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g := by
```

This isn't a `simp` lemma; it isn't entirely clear whether equality of functions or of particular values should necessarily be considered simpler, and making it a `simp` lemma introduces a `simpNF` linter failure for `eq_rec_inj`.

From AperiodicMonotilesLean.

Mathlib/Logic/Function/Basic.lean

@@ -78,6 +78,12 @@ theorem ne_iff {β : α → Sort*} {f₁ f₂ : ∀ a, β a} : f₁ ≠ f₂ ↔
   funext_iff.not.trans not_forall
 #align function.ne_iff Function.ne_iff
 
+lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
+    f x = g y ↔ f = g := by
+  refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩
+  · rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h
+  · rw [h, Subsingleton.elim x y]
+
 protected theorem Bijective.injective {f : α → β} (hf : Bijective f) : Injective f := hf.1
 #align function.bijective.injective Function.Bijective.injective
 protected theorem Bijective.surjective {f : α → β} (hf : Bijective f) : Surjective f := hf.2