From ee7bea2f8f8761352c0e26f1a8b656d510f3ddea Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 9 Aug 2023 20:24:01 +0000 Subject: [PATCH] chore(Algebra/Quandle): use `FunLike` (#6463) --- Mathlib/Algebra/Quandle.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/Quandle.lean b/Mathlib/Algebra/Quandle.lean index 85cf6973b9af0..b59f15f839395 100644 --- a/Mathlib/Algebra/Quandle.lean +++ b/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 :=