feat: a relation is "function-like" iff it is given by (f · = ·) (#…

…8190)

Partially inspired by [this thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Is.20False.20.E2.86.92.20p.20an.20axiom.20in.20Lean.204.20.3F) on Zulip.

Mathlib/Logic/Function/Basic.lean

@@ -934,6 +934,10 @@ protected theorem eq_iff {x y : α} : f x = y ↔ x = f y :=
 
 end Involutive
 
+@[simp]
+lemma symmetric_apply_eq_iff {f : α → α} : Symmetric (f · = ·) ↔ Involutive f := by
+  simp [Symmetric, Involutive]
+
 /-- The property of a binary function `f : α → β → γ` being injective.
 Mathematically this should be thought of as the corresponding function `α × β → γ` being injective.
 -/
@@ -1003,6 +1007,40 @@ end Sometimes
 
 end Function
 
+/-- A relation `r : α → β → Prop` is "function-like"
+(for each `a` there exists a unique `b` such that `r a b`)
+if and only if it is `(f · = ·)` for some function `f`. -/
+lemma forall_existsUnique_iff {r : α → β → Prop} :
+    (∀ a, ∃! b, r a b) ↔ ∃ f : α → β, ∀ {a b}, r a b ↔ f a = b := by
+  refine ⟨fun h ↦ ?_, ?_⟩
+  · refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
+    exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]
+  · rintro ⟨f, hf⟩
+    simp [hf]
+
+/-- A relation `r : α → β → Prop` is "function-like"
+(for each `a` there exists a unique `b` such that `r a b`)
+if and only if it is `(f · = ·)` for some function `f`. -/
+lemma forall_existsUnique_iff' {r : α → β → Prop} :
+    (∀ a, ∃! b, r a b) ↔ ∃ f : α → β, r = (f · = ·) := by
+  simp [forall_existsUnique_iff, Function.funext_iff]
+
+/-- A symmetric relation `r : α → α → Prop` is "function-like"
+(for each `a` there exists a unique `b` such that `r a b`)
+if and only if it is `(f · = ·)` for some involutive function `f`. -/
+protected lemma Symmetric.forall_existsUnique_iff' {r : α → α → Prop} (hr : Symmetric r) :
+    (∀ a, ∃! b, r a b) ↔ ∃ f : α → α, Involutive f ∧ r = (f · = ·) := by
+  refine ⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩
+  rcases forall_existsUnique_iff'.1 h with ⟨f, rfl : r = _⟩
+  exact ⟨f, symmetric_apply_eq_iff.1 hr, rfl⟩
+
+/-- A symmetric relation `r : α → α → Prop` is "function-like"
+(for each `a` there exists a unique `b` such that `r a b`)
+if and only if it is `(f · = ·)` for some involutive function `f`. -/
+protected lemma Symmetric.forall_existsUnique_iff {r : α → α → Prop} (hr : Symmetric r) :
+    (∀ a, ∃! b, r a b) ↔ ∃ f : α → α, Involutive f ∧ ∀ {a b}, r a b ↔ f a = b := by
+  simp [hr.forall_existsUnique_iff', funext_iff]
+
 /-- `s.piecewise f g` is the function equal to `f` on the set `s`, and to `g` on its complement. -/
 def Set.piecewise {α : Type u} {β : α → Sort v} (s : Set α) (f g : ∀ i, β i)
     [∀ j, Decidable (j ∈ s)] : ∀ i, β i :=