From 3a8f9db97b4e63efebebcd084ba40b6dee6a4359 Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Fri, 23 Apr 2021 11:01:59 +0000
Subject: [PATCH] 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 | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/logic/function/basic.lean b/src/logic/function/basic.lean
index dbc798877e872..c0ddb8d55cc7c 100644
--- a/src/logic/function/basic.lean
+++ b/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.