chore(Algebra/Quandle): use FunLike (#6463)

Mathlib/Algebra/Quandle.lean

@@ -358,14 +358,12 @@ namespace ShelfHom
 
 variable {S₁ : Type _} {S₂ : Type _} {S₃ : Type _} [Shelf S₁] [Shelf S₂] [Shelf S₃]
 
-instance : CoeFun (S₁ →◃ S₂) fun _ => S₁ → S₂ :=
-  ⟨ShelfHom.toFun⟩
-
--- Porting Note: Syntactically equal in Lean4
--- @[simp]
--- theorem toFun_eq_coe (f : S₁ →◃ S₂) : f.toFun = f :=
---   rfl
-#noalign shelf_hom.to_fun_eq_coe
+instance : FunLike (S₁ →◃ S₂) S₁ fun _ => S₂ where
+  coe := toFun
+  coe_injective' | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+@[simp] theorem toFun_eq_coe (f : S₁ →◃ S₂) : f.toFun = f := rfl
+#align shelf_hom.to_fun_eq_coe ShelfHom.toFun_eq_coe
 
 @[simp]
 theorem map_act (f : S₁ →◃ S₂) {x y : S₁} : f (x ◃ y) = f x ◃ f y :=