feat(logic/function/basic): function.involutive.eq_iff (#7332)

The lemma name matches the brevity of `function.injective.eq_iff`.
The fact the definitions differ isn't important, as both are accessible from `hf : involutive f` as `hf.eq_iff` and `hf.injective.eq_iff`.

src/logic/function/basic.lean

@@ -571,6 +571,10 @@ protected lemma ite_not (P : Prop) [decidable P] (x : α) :
   f (ite P x (f x)) = ite (¬ P) x (f x) :=
 by rw [apply_ite f, h, ite_not]
 
+/-- An involution commutes across an equality. Compare to `function.injective.eq_iff`. -/
+protected lemma eq_iff {x y : α} : f x = y ↔ x = f y :=
+h.injective.eq_iff' (h y)
+
 end involutive
 
 /-- The property of a binary function `f : α → β → γ` being injective.