chore(algebra/category/*): simp lemmas for of_hom (#12638)

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

Author: kim-em

src/algebra/category/Algebra/basic.lean

@@ -62,6 +62,10 @@ def of (X : Type v) [ring X] [algebra R X] : Algebra.{v} R := ⟨X⟩
 def of_hom {R : Type u} [comm_ring R] {X Y : Type v} [ring X] [algebra R X] [ring Y] [algebra R Y]
   (f : X →ₐ[R] Y) : of R X ⟶ of R Y := f
 
+@[simp] lemma of_hom_apply {R : Type u} [comm_ring R]
+  {X Y : Type v} [ring X] [algebra R X] [ring Y] [algebra R Y] (f : X →ₐ[R] Y) (x : X) :
+  of_hom f x = f x := rfl
+
 instance : inhabited (Algebra R) := ⟨of R R⟩
 
 @[simp]

src/algebra/category/CommRing/basic.lean

@@ -47,6 +47,9 @@ def of (R : Type u) [semiring R] : SemiRing := bundled.of R
 /-- Typecheck a `ring_hom` as a morphism in `SemiRing`. -/
 def of_hom {R S : Type u} [semiring R] [semiring S] (f : R →+* S) : of R ⟶ of S := f
 
+@[simp] lemma of_hom_apply {R S : Type u} [semiring R] [semiring S] (f : R →+* S) (x : R) :
+  of_hom f x = f x := rfl
+
 instance : inhabited SemiRing := ⟨of punit⟩
 
 instance (R : SemiRing) : semiring R := R.str
@@ -81,6 +84,9 @@ def of (R : Type u) [ring R] : Ring := bundled.of R
 /-- Typecheck a `ring_hom` as a morphism in `Ring`. -/
 def of_hom {R S : Type u} [ring R] [ring S] (f : R →+* S) : of R ⟶ of S := f
 
+@[simp] lemma of_hom_apply {R S : Type u} [ring R] [ring S] (f : R →+* S) (x : R) :
+  of_hom f x = f x := rfl
+
 instance : inhabited Ring := ⟨of punit⟩
 
 instance (R : Ring) : ring R := R.str
@@ -113,6 +119,10 @@ def of (R : Type u) [comm_semiring R] : CommSemiRing := bundled.of R
 /-- Typecheck a `ring_hom` as a morphism in `CommSemiRing`. -/
 def of_hom {R S : Type u} [comm_semiring R] [comm_semiring S] (f : R →+* S) : of R ⟶ of S := f
 
+@[simp]
+lemma of_hom_apply {R S : Type u} [comm_semiring R] [comm_semiring S] (f : R →+* S) (x : R) :
+  of_hom f x = f x := rfl
+
 instance : inhabited CommSemiRing := ⟨of punit⟩
 
 instance (R : CommSemiRing) : comm_semiring R := R.str
@@ -146,6 +156,9 @@ def of (R : Type u) [comm_ring R] : CommRing := bundled.of R
 /-- Typecheck a `ring_hom` as a morphism in `CommRing`. -/
 def of_hom {R S : Type u} [comm_ring R] [comm_ring S] (f : R →+* S) : of R ⟶ of S := f
 
+@[simp] lemma of_hom_apply {R S : Type u} [comm_ring R] [comm_ring S] (f : R →+* S) (x : R) :
+  of_hom f x = f x := rfl
+
 instance : inhabited CommRing := ⟨of punit⟩
 
 instance (R : CommRing) : comm_ring R := R.str

src/algebra/category/Group/basic.lean

@@ -50,6 +50,9 @@ add_decl_doc AddGroup.of
 /-- Typecheck a `add_monoid_hom` as a morphism in `AddGroup`. -/
 add_decl_doc AddGroup.of_hom
 
+@[simp, to_additive] lemma of_hom_apply {X Y : Type*} [group X] [group Y] (f : X →* Y) (x : X) :
+  of_hom f x = f x := rfl
+
 @[to_additive]
 instance (G : Group) : group G := G.str
 
@@ -112,6 +115,9 @@ add_decl_doc AddCommGroup.of
 /-- Typecheck a `add_monoid_hom` as a morphism in `AddCommGroup`. -/
 add_decl_doc AddCommGroup.of_hom
 
+@[simp, to_additive] lemma of_hom_apply {X Y : Type*} [comm_group X] [comm_group Y] (f : X →* Y)
+  (x : X) : of_hom f x = f x := rfl
+
 @[to_additive]
 instance comm_group_instance (G : CommGroup) : comm_group G := G.str
 

src/algebra/category/Module/basic.lean

@@ -112,6 +112,10 @@ rfl
 def of_hom {R : Type u} [ring R] {X Y : Type v} [add_comm_group X] [module R X] [add_comm_group Y]
   [module R Y] (f : X →ₗ[R] Y) : of R X ⟶ of R Y := f
 
+@[simp] lemma of_hom_apply {R : Type u} [ring R]
+  {X Y : Type v} [add_comm_group X] [module R X] [add_comm_group Y] [module R Y] (f : X →ₗ[R] Y)
+  (x : X) : of_hom f x = f x := rfl
+
 instance : has_zero (Module R) := ⟨of R punit⟩
 instance : inhabited (Module R) := ⟨0⟩
 

src/algebra/category/Mon/basic.lean

@@ -64,6 +64,9 @@ add_decl_doc AddMon.of
 /-- Typecheck a `add_monoid_hom` as a morphism in `AddMon`. -/
 add_decl_doc AddMon.of_hom
 
+@[simp] lemma of_hom_apply {X Y : Type u} [monoid X] [monoid Y] (f : X →* Y)
+  (x : X) : of_hom f x = f x := rfl
+
 @[to_additive]
 instance : inhabited Mon :=
 -- The default instance for `monoid punit` is derived via `punit.comm_ring`,

src/algebra/category/Semigroup/basic.lean

@@ -61,6 +61,9 @@ add_decl_doc AddMagma.of
 /-- Typecheck a `add_hom` as a morphism in `AddMagma`. -/
 add_decl_doc AddMagma.of_hom
 
+@[simp, to_additive] lemma of_hom_apply {X Y : Type u} [has_mul X] [has_mul Y] (f : mul_hom X Y)
+  (x : X) : of_hom f x = f x := rfl
+
 @[to_additive]
 instance : inhabited Magma := ⟨Magma.of pempty⟩
 
@@ -102,6 +105,9 @@ add_decl_doc AddSemigroup.of
 /-- Typecheck a `add_hom` as a morphism in `AddSemigroup`. -/
 add_decl_doc AddSemigroup.of_hom
 
+@[simp, to_additive] lemma of_hom_apply {X Y : Type u} [semigroup X] [semigroup Y] (f : mul_hom X Y)
+  (x : X) : of_hom f x = f x := rfl
+
 @[to_additive]
 instance : inhabited Semigroup := ⟨Semigroup.of pempty⟩