fix(Logic/Embedding/Basic): Generalise arrowCongrRight_apply (#10739)

`f` does not need to be an embedding, and this version is syntactically strictly more general.

Author: FLDutchmann

Mathlib/Logic/Embedding/Basic.lean

@@ -367,7 +367,7 @@ def arrowCongrRight {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) :
 #align function.embedding.arrow_congr_right Function.Embedding.arrowCongrRight
 
 @[simp]
-theorem arrowCongrRight_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) (f : γ ↪ α) :
+theorem arrowCongrRight_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) (f : γ → α) :
     arrowCongrRight e f = e ∘ f :=
   rfl
 #align function.embedding.arrow_congr_right_apply Function.Embedding.arrowCongrRight_apply