feat(logic/embedding): simp lemma for injectivity for embeddings (#7881)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Author: kim-em

src/logic/embedding.lean

@@ -66,6 +66,9 @@ by { ext, simp }
 
 theorem injective {α β} (f : α ↪ β) : injective f := f.inj'
 
+@[simp] lemma apply_eq_iff_eq {α β : Type*} (f : α ↪ β) (x y : α) : f x = f y ↔ x = y :=
+f.injective.eq_iff
+
 @[refl, simps {simp_rhs := tt}]
 protected def refl (α : Sort*) : α ↪ α :=
 ⟨id, injective_id⟩