From 237c33e0aaec18b06e7389bf0c850f5aa911e796 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Fri, 12 May 2023 11:43:07 +0000
Subject: [PATCH] chore: refactor of concrete categories (#3900)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

I think the ports
* https://github.com/leanprover-community/mathlib4/pull/2902 (MonCat)
* https://github.com/leanprover-community/mathlib4/pull/3036 (GroupCat)
* https://github.com/leanprover-community/mathlib4/pull/3260 (ModuleCat)

didn't quite get things right, and also have some variation between them. This PR tries to straighten things out.

Major changes:
* Have the coercion to type be via `X.\a`, and put attribute `@[coe]` on this.
* Make sure the coercion from morphisms to functions means that simp lemmas about the underlying bundled morphisms apply directly.
  * This means we drop lemmas like
  ```
  lemma Hom.map_mul {X Y : MonCat} (f : X ⟶ Y) (x y : X) : ((forget MonCat).map f) (x * y) = f x * f y
   ```
   * But at the expense of adding lemmas like
   ```
   lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
   ```

Overall I'm pretty happy, and it allows me to unstick the long stuck https://github.com/leanprover-community/mathlib4/pull/3105.

This is not everything I want to do to refactor these files, but once I was satisfied that I can move forward with RingCat, I want to get this merged so we can unblock porting progress. I'll promise to come back to this soon! :-)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
---
 Mathlib/Algebra/Category/GroupCat/Basic.lean  | 328 +++++++-----------
 .../Algebra/Category/GroupCat/EpiMono.lean    |   7 +-
 Mathlib/Algebra/Category/GroupCat/Zero.lean   |   4 +-
 Mathlib/Algebra/Category/ModuleCat/Basic.lean |  22 +-
 .../Algebra/Category/ModuleCat/Tannaka.lean   |   4 +-
 Mathlib/Algebra/Category/MonCat/Basic.lean    | 213 ++++++------
 .../AlgebraicTopology/SimplexCategory.lean    |   2 +-
 .../AlgebraicTopology/TopologicalSimplex.lean |   6 +-
 .../CategoryTheory/Category/Bipointed.lean    |   2 +-
 Mathlib/CategoryTheory/Category/Pointed.lean  |   2 +-
 .../ConcreteCategory/Basic.lean               |  30 +-
 .../ConcreteCategory/Bundled.lean             |   3 +
 .../ConcreteCategory/BundledHom.lean          |   2 +-
 Mathlib/CategoryTheory/GradedObject.lean      |   2 +-
 .../Preadditive/Yoneda/Basic.lean             |   8 +-
 .../Order/Category/NonemptyFinLinOrdCat.lean  |   2 +-
 Mathlib/Tactic/Elementwise.lean               |   2 +-
 .../Category/CompHaus/Projective.lean         |   2 +-
 .../Category/Profinite/Projective.lean        |   2 +-
 Mathlib/Topology/Category/Top/Basic.lean      |   4 +-
 20 files changed, 286 insertions(+), 361 deletions(-)

diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean
index dedce71c0ee58..6098f6c319348 100644
--- a/Mathlib/Algebra/Category/GroupCat/Basic.lean
+++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean
@@ -45,20 +45,40 @@ namespace GroupCat
 instance : BundledHom.ParentProjection
   (fun {α : Type _} (h : Group α) => h.toDivInvMonoid.toMonoid) := ⟨⟩
 
-instance largeCategory : LargeCategory GroupCat := by
-  dsimp only [GroupCat]
-  infer_instance
+deriving instance LargeCategory for GroupCat
+attribute [to_additive] instGroupCatLargeCategory
 
+@[to_additive]
 instance concreteCategory : ConcreteCategory GroupCat := by
   dsimp only [GroupCat]
   infer_instance
 
-attribute [to_additive] GroupCat.largeCategory GroupCat.concreteCategory
+@[to_additive]
+instance : CoeSort GroupCat (Type _) where
+  coe X := X.α
 
 @[to_additive]
-instance : CoeSort GroupCat (Type _) := by
-  dsimp only [GroupCat]
-  infer_instance
+instance (X : GroupCat) : Group X := X.str
+
+-- porting note: this instance was not necessary in mathlib
+@[to_additive]
+instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
+  coe (f : X →* Y) := f
+
+-- porting note: added
+@[to_additive (attr := simp)]
+lemma coe_id {X : GroupCat} : (𝟙 X : X → X) = id := rfl
+
+-- porting note: added
+@[to_additive (attr := simp)]
+lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
+
+-- porting note: added
+@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl
+
+@[to_additive (attr := ext)]
+lemma ext {X Y : GroupCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
+  MonoidHom.ext w
 
 /-- Construct a bundled `Group` from the underlying type and typeclass. -/
 @[to_additive]
@@ -72,53 +92,7 @@ set_option linter.uppercaseLean3 false in
 /-- Construct a bundled `AddGroup` from the underlying type and typeclass. -/
 add_decl_doc AddGroupCat.of
 
-/-- Typecheck a `MonoidHom` as a morphism in `GroupCat`. -/
-@[to_additive]
-def ofHom {X Y : Type u} [Group X] [Group Y] (f : X →* Y) : of X ⟶ of Y :=
-  f
-set_option linter.uppercaseLean3 false in
-#align Group.of_hom GroupCat.ofHom
-set_option linter.uppercaseLean3 false in
-#align AddGroup.of_hom AddGroupCat.ofHom
-
-/-- Typecheck a `AddMonoidHom` as a morphism in `AddGroup`. -/
-add_decl_doc AddGroupCat.ofHom
-
--- porting note: this instance was not necessary in mathlib
-@[to_additive]
-instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y :=
-  ConcreteCategory.hasCoeToFun
-
--- porting note: this was added to ease automation
-@[to_additive (attr := simp)]
-lemma id_apply {X : GroupCat} (x : X) :
-  (𝟙 X) x = x := rfl
-
--- porting note: this was added to ease automation
 @[to_additive (attr := simp)]
-lemma comp_apply {X Y Z : GroupCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
-  (f ≫ g) x = g (f x) := rfl
-
-@[to_additive (attr := simp)]
-theorem ofHom_apply {X Y : Type _} [Group X] [Group Y] (f : X →* Y) (x : X) :
-    (ofHom f) x = f x :=
-  rfl
-set_option linter.uppercaseLean3 false in
-#align Group.of_hom_apply GroupCat.ofHom_apply
-set_option linter.uppercaseLean3 false in
-#align AddGroup.of_hom_apply AddGroupCat.ofHom_apply
-
-@[to_additive]
-instance (G : GroupCat) : Group G :=
-  G.str
-
--- porting note: added to make `one_apply` work
-@[to_additive]
-instance (G : GroupCat) : Group ((forget GroupCat).obj G) :=
-  G.str
-
--- porting note: simp attribute was removed to please the linter
-@[to_additive]
 theorem coe_of (R : Type u) [Group R] : ↑(GroupCat.of R) = R :=
   rfl
 set_option linter.uppercaseLean3 false in
@@ -130,66 +104,60 @@ set_option linter.uppercaseLean3 false in
 instance : Inhabited GroupCat :=
   ⟨GroupCat.of PUnit⟩
 
-@[to_additive]
-instance ofUnique (G : Type _) [Group G] [i : Unique G] : Unique (GroupCat.of G) :=
-  i
+@[to_additive hasForgetToAddMonCat]
+instance hasForgetToMonCat : HasForget₂ GroupCat MonCat :=
+  BundledHom.forget₂ _ _
 set_option linter.uppercaseLean3 false in
-#align Group.of_unique GroupCat.ofUnique
+#align Group.has_forget_to_Mon GroupCat.hasForgetToMonCat
 set_option linter.uppercaseLean3 false in
-#align AddGroup.of_unique AddGroupCat.ofUnique
+#align AddGroup.has_forget_to_AddMon AddGroupCat.hasForgetToAddMonCat
+
+@[to_additive]
+instance : Coe GroupCat.{u} MonCat.{u} where coe := (forget₂ GroupCat MonCat).obj
 
 -- porting note: this instance was not necessary in mathlib
 @[to_additive]
 instance (G H : GroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
 
 @[to_additive (attr := simp)]
-theorem one_apply (G H : GroupCat) (g : G) : ((forget GroupCat).map (1 : G ⟶ H)) g = 1 :=
+theorem one_apply (G H : GroupCat) (g : G) : ((1 : G ⟶ H) : G → H) g = 1 :=
   rfl
 set_option linter.uppercaseLean3 false in
 #align Group.one_apply GroupCat.one_apply
 set_option linter.uppercaseLean3 false in
 #align AddGroup.zero_apply AddGroupCat.zero_apply
 
-@[to_additive (attr := ext)]
-theorem ext (G H : GroupCat) (f₁ f₂ : G ⟶ H) (w : ∀ (x : ↑G), f₁ x = f₂ x) : f₁ = f₂ :=
-  ConcreteCategory.hom_ext _ _ w
+/-- Typecheck a `MonoidHom` as a morphism in `GroupCat`. -/
+@[to_additive]
+def ofHom {X Y : Type u} [Group X] [Group Y] (f : X →* Y) : of X ⟶ of Y :=
+  f
 set_option linter.uppercaseLean3 false in
-#align Group.ext GroupCat.ext
+#align Group.of_hom GroupCat.ofHom
 set_option linter.uppercaseLean3 false in
-#align AddGroup.ext AddGroupCat.ext
+#align AddGroup.of_hom AddGroupCat.ofHom
 
-@[to_additive hasForgetToAddMonCat]
-instance hasForgetToMonCat : HasForget₂ GroupCat MonCat :=
-  BundledHom.forget₂ _ _
+/-- Typecheck a `AddMonoidHom` as a morphism in `AddGroup`. -/
+add_decl_doc AddGroupCat.ofHom
+
+@[to_additive (attr := simp)]
+theorem ofHom_apply {X Y : Type _} [Group X] [Group Y] (f : X →* Y) (x : X) :
+    (ofHom f) x = f x :=
+  rfl
 set_option linter.uppercaseLean3 false in
-#align Group.has_forget_to_Mon GroupCat.hasForgetToMonCat
+#align Group.of_hom_apply GroupCat.ofHom_apply
 set_option linter.uppercaseLean3 false in
-#align AddGroup.has_forget_to_AddMon AddGroupCat.hasForgetToAddMonCat
+#align AddGroup.of_hom_apply AddGroupCat.ofHom_apply
 
 @[to_additive]
-instance : Coe GroupCat.{u} MonCat.{u} where coe := (forget₂ GroupCat MonCat).obj
+instance ofUnique (G : Type _) [Group G] [i : Unique G] : Unique (GroupCat.of G) := i
+set_option linter.uppercaseLean3 false in
+#align Group.of_unique GroupCat.ofUnique
+set_option linter.uppercaseLean3 false in
+#align AddGroup.of_unique AddGroupCat.ofUnique
 
--- porting note: this was added to ease the port
-/-- the morphism in `GroupCat` associated to a `MonoidHom` -/
+-- We verify that simp lemmas apply when coercing morphisms to functions.
 @[to_additive]
-def Hom.mk {X Y : GroupCat} (f : X →* Y) : X ⟶ Y := f
-
-/-- the morphism in `AddGroupCat` associated to a `AddMonoidHom` -/
-add_decl_doc AddGroupCat.Hom.mk
-
-@[to_additive (attr := simp)]
-lemma Hom.mk_apply {X Y : GroupCat} (f : X →* Y) (x : X) :
-  (Hom.mk f) x = f x := rfl
-
--- porting note: added to ease automation
-@[to_additive (attr := simp)]
-lemma Hom.map_mul {X Y : GroupCat} (f : X ⟶ Y) (x y : X) : f (x * y) = f x * f y := by
-  apply MonoidHom.map_mul (show MonoidHom X Y from f)
-
--- porting note: added to ease automation
-@[to_additive (attr := simp)]
-lemma Hom.map_one {X Y : GroupCat} (f : X ⟶ Y) : f (1 : X) = 1 := by
-  apply MonoidHom.map_one (show MonoidHom X Y from f)
+example {R S : GroupCat} (i : R ⟶ S) (r : R) (h : r = 1) : i r = 1 := by simp [h]
 
 end GroupCat
 
@@ -206,89 +174,76 @@ set_option linter.uppercaseLean3 false in
 add_decl_doc AddCommGroupCat
 
 /-- `Ab` is an abbreviation for `AddCommGroup`, for the sake of mathematicians' sanity. -/
-abbrev Ab :=
-  AddCommGroupCat
+abbrev Ab := AddCommGroupCat
 set_option linter.uppercaseLean3 false in
 #align Ab Ab
 
 namespace CommGroupCat
 
 @[to_additive]
-instance : BundledHom.ParentProjection @CommGroup.toGroup :=
-  ⟨⟩
+instance : BundledHom.ParentProjection @CommGroup.toGroup := ⟨⟩
 
-instance largeCategory : LargeCategory CommGroupCat := by
-  dsimp only [CommGroupCat]
-  infer_instance
-
-instance concreteCategory : ConcreteCategory CommGroupCat := by
-  dsimp only [CommGroupCat]
-  infer_instance
-
-attribute [to_additive] CommGroupCat.largeCategory CommGroupCat.concreteCategory
+deriving instance LargeCategory for CommGroupCat
+attribute [to_additive] instCommGroupCatLargeCategory
 
 @[to_additive]
-instance : CoeSort CommGroupCat (Type _) := by
+instance concreteCategory : ConcreteCategory CommGroupCat := by
   dsimp only [CommGroupCat]
   infer_instance
 
-/-- Construct a bundled `CommGroup` from the underlying type and typeclass. -/
 @[to_additive]
-def of (G : Type u) [CommGroup G] : CommGroupCat :=
-  Bundled.of G
-set_option linter.uppercaseLean3 false in
-#align CommGroup.of CommGroupCat.of
-set_option linter.uppercaseLean3 false in
-#align AddCommGroup.of AddCommGroupCat.of
-
-/-- Construct a bundled `AddCommGroup` from the underlying type and typeclass. -/
-add_decl_doc AddCommGroupCat.of
+instance : CoeSort CommGroupCat (Type _) where
+  coe X := X.α
 
-/-- Typecheck a `MonoidHom` as a morphism in `CommGroup`. -/
 @[to_additive]
-def ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : of X ⟶ of Y :=
-  f
+instance commGroupInstance (X : CommGroupCat) : CommGroup X := X.str
 set_option linter.uppercaseLean3 false in
-#align CommGroup.of_hom CommGroupCat.ofHom
+#align CommGroup.comm_group_instance CommGroupCat.commGroupInstance
 set_option linter.uppercaseLean3 false in
-#align AddCommGroup.of_hom AddCommGroupCat.ofHom
-
-/-- Typecheck a `AddMonoidHom` as a morphism in `AddCommGroup`. -/
-add_decl_doc AddCommGroupCat.ofHom
+#align AddCommGroup.add_comm_group_instance AddCommGroupCat.addCommGroupInstance
 
 -- porting note: this instance was not necessary in mathlib
 @[to_additive]
-instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y :=
-  ConcreteCategory.hasCoeToFun
+instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
+  coe (f : X →* Y) := f
 
--- porting note: added to ease automation
+-- porting note: added
 @[to_additive (attr := simp)]
-lemma id_apply {X : CommGroupCat} (x : X) :
-  (𝟙 X) x = x := rfl
+lemma coe_id {X : CommGroupCat} : (𝟙 X : X → X) = id := rfl
 
--- porting note: added to ease automation
+-- porting note: added
 @[to_additive (attr := simp)]
-lemma comp_apply {X Y Z : CommGroupCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
-  (f ≫ g) x = g (f x) := by apply CategoryTheory.comp_apply
+lemma coe_comp {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
+-- porting note: added
 @[to_additive (attr := simp)]
-theorem ofHom_apply {X Y : Type _} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) :
-    (ofHom f) x = f x :=
+lemma forget_map {X Y : CommGroupCat} (f : X ⟶ Y) :
+    (forget CommGroupCat).map f = (f : X → Y) :=
   rfl
-set_option linter.uppercaseLean3 false in
-#align CommGroup.of_hom_apply CommGroupCat.ofHom_apply
-set_option linter.uppercaseLean3 false in
-#align AddCommGroup.of_hom_apply AddCommGroupCat.ofHom_apply
 
+@[to_additive (attr := ext)]
+lemma ext {X Y : CommGroupCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
+  MonoidHom.ext w
+
+/-- Construct a bundled `CommGroup` from the underlying type and typeclass. -/
 @[to_additive]
-instance commGroupInstance (G : CommGroupCat) : CommGroup G :=
-  G.str
+def of (G : Type u) [CommGroup G] : CommGroupCat :=
+  Bundled.of G
 set_option linter.uppercaseLean3 false in
-#align CommGroup.comm_group_instance CommGroupCat.commGroupInstance
+#align CommGroup.of CommGroupCat.of
 set_option linter.uppercaseLean3 false in
-#align AddCommGroup.add_comm_group_instance AddCommGroupCat.addCommGroupInstance
+#align AddCommGroup.of AddCommGroupCat.of
+
+/-- Construct a bundled `AddCommGroup` from the underlying type and typeclass. -/
+add_decl_doc AddCommGroupCat.of
+
+@[to_additive]
+instance : Inhabited CommGroupCat :=
+  ⟨CommGroupCat.of PUnit⟩
 
--- porting note: simp attribute was removed to please the linter
+-- Porting note: removed `@[simp]` here, as it makes it harder to tell when to apply
+-- bundled or unbundled lemmas.
+-- (This change seems dangerous!)
 @[to_additive]
 theorem coe_of (R : Type u) [CommGroup R] : (CommGroupCat.of R : Type u) = R :=
   rfl
@@ -297,10 +252,6 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.coe_of AddCommGroupCat.coe_of
 
-@[to_additive]
-instance : Inhabited CommGroupCat :=
-  ⟨CommGroupCat.of PUnit⟩
-
 @[to_additive]
 instance ofUnique (G : Type _) [CommGroup G] [i : Unique G] : Unique (CommGroupCat.of G) :=
   i
@@ -309,26 +260,6 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.of_unique AddCommGroupCat.ofUnique
 
--- porting note: this instance was not necessary in mathlib
-@[to_additive]
-instance (G H : CommGroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
-
-@[to_additive (attr := simp)]
-theorem one_apply (G H : CommGroupCat) (g : G) : (1 : G ⟶ H) g = 1 :=
-  rfl
-set_option linter.uppercaseLean3 false in
-#align CommGroup.one_apply CommGroupCat.one_apply
-set_option linter.uppercaseLean3 false in
-#align AddCommGroup.zero_apply AddCommGroupCat.zero_apply
-
-@[to_additive (attr := ext)]
-theorem ext (G H : CommGroupCat) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
-  ConcreteCategory.hom_ext _ _ w
-set_option linter.uppercaseLean3 false in
-#align CommGroup.ext CommGroupCat.ext
-set_option linter.uppercaseLean3 false in
-#align AddCommGroup.ext AddCommGroupCat.ext
-
 @[to_additive]
 instance hasForgetToGroup : HasForget₂ CommGroupCat GroupCat :=
   BundledHom.forget₂ _ _
@@ -351,33 +282,40 @@ set_option linter.uppercaseLean3 false in
 @[to_additive]
 instance : Coe CommGroupCat.{u} CommMonCat.{u} where coe := (forget₂ CommGroupCat CommMonCat).obj
 
--- porting note: this was added to ease the port
-/-- the morphism in `CommGroupCat` associated to a `MonoidHom` -/
+-- porting note: this instance was not necessary in mathlib
 @[to_additive]
-def Hom.mk {X Y : CommGroupCat} (f : X →* Y) : X ⟶ Y := f
-
-/-- the morphism in `AddCommGroupCat` associated to a `AddMonoidHom` -/
-add_decl_doc AddCommGroupCat.Hom.mk
+instance (G H : CommGroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
 
 @[to_additive (attr := simp)]
-lemma Hom.mk_apply {X Y : CommGroupCat} (f : X →* Y) (x : X) :
-  (Hom.mk f) x = f x := rfl
+theorem one_apply (G H : CommGroupCat) (g : G) : ((1 : G ⟶ H) : G → H) g = 1 :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align CommGroup.one_apply CommGroupCat.one_apply
+set_option linter.uppercaseLean3 false in
+#align AddCommGroup.zero_apply AddCommGroupCat.zero_apply
 
--- porting note: added to ease automation
-@[to_additive (attr := simp)]
-lemma Hom.map_mul {X Y : CommGroupCat} (f : X ⟶ Y) (x y : X) : f (x * y) = f x * f y := by
-  apply MonoidHom.map_mul (show MonoidHom X Y from f)
+/-- Typecheck a `MonoidHom` as a morphism in `CommGroup`. -/
+@[to_additive]
+def ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) : of X ⟶ of Y :=
+  f
+set_option linter.uppercaseLean3 false in
+#align CommGroup.of_hom CommGroupCat.ofHom
+set_option linter.uppercaseLean3 false in
+#align AddCommGroup.of_hom AddCommGroupCat.ofHom
+
+/-- Typecheck a `AddMonoidHom` as a morphism in `AddCommGroup`. -/
+add_decl_doc AddCommGroupCat.ofHom
 
--- porting note: added to ease automation
 @[to_additive (attr := simp)]
-lemma Hom.map_one {X Y : CommGroupCat} (f : X ⟶ Y) : f (1 : X) = 1 := by
-  apply MonoidHom.map_one (show MonoidHom X Y from f)
+theorem ofHom_apply {X Y : Type _} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) :
+    (ofHom f) x = f x :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align CommGroup.of_hom_apply CommGroupCat.ofHom_apply
+set_option linter.uppercaseLean3 false in
+#align AddCommGroup.of_hom_apply AddCommGroupCat.ofHom_apply
 
--- Porting note: is this still relevant?
--- This example verifies an improvement possible in Lean 3.8.
--- Before that, to have `MonoidHom.map_map` usable by `simp` here,
--- we had to mark all the concrete category `CoeSort` instances reducible.
--- Now, it just works.
+-- We verify that simp lemmas apply when coercing morphisms to functions.
 @[to_additive]
 example {R S : CommGroupCat} (i : R ⟶ S) (r : R) (h : r = 1) : i r = 1 := by simp [h]
 
@@ -430,8 +368,8 @@ end AddCommGroupCat
 /-- Build an isomorphism in the category `GroupCat` from a `MulEquiv` between `Group`s. -/
 @[to_additive (attr := simps)]
 def MulEquiv.toGroupCatIso {X Y : GroupCat} (e : X ≃* Y) : X ≅ Y where
-  hom := GroupCat.Hom.mk e.toMonoidHom
-  inv := GroupCat.Hom.mk e.symm.toMonoidHom
+  hom := e.toMonoidHom
+  inv := e.symm.toMonoidHom
 set_option linter.uppercaseLean3 false in
 #align mul_equiv.to_Group_iso MulEquiv.toGroupCatIso
 set_option linter.uppercaseLean3 false in
@@ -444,8 +382,8 @@ add_decl_doc AddEquiv.toAddGroupCatIso
 between `CommGroup`s. -/
 @[to_additive (attr := simps)]
 def MulEquiv.toCommGroupCatIso {X Y : CommGroupCat} (e : X ≃* Y) : X ≅ Y where
-  hom := CommGroupCat.Hom.mk e.toMonoidHom
-  inv := CommGroupCat.Hom.mk e.symm.toMonoidHom
+  hom := e.toMonoidHom
+  inv := e.symm.toMonoidHom
 set_option linter.uppercaseLean3 false in
 #align mul_equiv.to_CommGroup_iso MulEquiv.toCommGroupCatIso
 set_option linter.uppercaseLean3 false in
@@ -518,11 +456,11 @@ namespace CategoryTheory.Aut
 /-- The (bundled) group of automorphisms of a type is isomorphic to the (bundled) group
 of permutations. -/
 def isoPerm {α : Type u} : GroupCat.of (Aut α) ≅ GroupCat.of (Equiv.Perm α) where
-  hom := GroupCat.Hom.mk
+  hom :=
     { toFun := fun g => g.toEquiv
       map_one' := by aesop
       map_mul' := by aesop }
-  inv := GroupCat.Hom.mk
+  inv :=
     { toFun := fun g => g.toIso
       map_one' := by aesop
       map_mul' := by aesop }
@@ -542,7 +480,9 @@ end CategoryTheory.Aut
 instance GroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget GroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget GroupCat).map f)
-    let e : X ≃* Y := MulEquiv.mk i.toEquiv (by apply GroupCat.Hom.map_mul)
+    let e : X ≃* Y := MulEquiv.mk i.toEquiv
+      -- Porting note: this would ideally be `by aesop`, as in `MonCat.forget_reflects_isos`
+      (MonoidHom.map_mul (show MonoidHom X Y from f))
     exact IsIso.of_iso e.toGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align Group.forget_reflects_isos GroupCat.forget_reflects_isos
@@ -553,7 +493,9 @@ set_option linter.uppercaseLean3 false in
 instance CommGroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommGroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget CommGroupCat).map f)
-    let e : X ≃* Y := MulEquiv.mk i.toEquiv (by apply CommGroupCat.Hom.map_mul)
+    let e : X ≃* Y := MulEquiv.mk i.toEquiv
+      -- Porting note: this would ideally be `by aesop`, as in `MonCat.forget_reflects_isos`
+      (MonoidHom.map_mul (show MonoidHom X Y from f))
     exact IsIso.of_iso e.toCommGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align CommGroup.forget_reflects_isos CommGroupCat.forget_reflects_isos
diff --git a/Mathlib/Algebra/Category/GroupCat/EpiMono.lean b/Mathlib/Algebra/Category/GroupCat/EpiMono.lean
index 306f31bd23173..2aeea07ff92f9 100644
--- a/Mathlib/Algebra/Category/GroupCat/EpiMono.lean
+++ b/Mathlib/Algebra/Category/GroupCat/EpiMono.lean
@@ -303,7 +303,6 @@ theorem agree : f.range.carrier = { x | h x = g x } := by
         simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m)]
         congr
         rw [leftCoset_assoc _ (f a) y]
-        rfl
       · rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
         simp only [leftCoset_assoc]
     · rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
@@ -324,7 +323,6 @@ theorem comp_eq : (f ≫ show B ⟶ GroupCat.of SX' from g) = f ≫ show B ⟶ G
   have : f a ∈ { b | h b = g b } := by
     rw [←agree]
     use a
-    rfl
   rw [this]
 #align Group.surjective_of_epi_auxs.comp_eq GroupCat.SurjectiveOfEpiAuxs.comp_eq
 
@@ -353,7 +351,7 @@ theorem surjective_of_epi [Epi f] : Function.Surjective f := by
 #align Group.surjective_of_epi GroupCat.surjective_of_epi
 
 theorem epi_iff_surjective : Epi f ↔ Function.Surjective f :=
-  ⟨fun _ => surjective_of_epi f, ConcreteCategory.epi_of_surjective _⟩
+  ⟨fun _ => surjective_of_epi f, ConcreteCategory.epi_of_surjective f⟩
 #align Group.epi_iff_surjective GroupCat.epi_iff_surjective
 
 theorem epi_iff_range_eq_top : Epi f ↔ f.range = ⊤ :=
@@ -454,8 +452,6 @@ theorem epi_iff_range_eq_top : Epi f ↔ f.range = ⊤ :=
 @[to_additive]
 theorem epi_iff_surjective : Epi f ↔ Function.Surjective f := by
   rw [epi_iff_range_eq_top, MonoidHom.range_top_iff_surjective]
-  -- Porting note: extra rfl forces the issue
-  rfl
 #align CommGroup.epi_iff_surjective CommGroupCat.epi_iff_surjective
 #align AddCommGroup.epi_iff_surjective AddCommGroupCat.epi_iff_surjective
 
@@ -474,4 +470,3 @@ instance forget_commGroupCat_preserves_epi : (forget CommGroupCat).PreservesEpim
 end CommGroupCat
 
 end
-
diff --git a/Mathlib/Algebra/Category/GroupCat/Zero.lean b/Mathlib/Algebra/Category/GroupCat/Zero.lean
index af59b2322f523..126e918d08f70 100644
--- a/Mathlib/Algebra/Category/GroupCat/Zero.lean
+++ b/Mathlib/Algebra/Category/GroupCat/Zero.lean
@@ -32,7 +32,7 @@ theorem isZero_of_subsingleton (G : GroupCat) [Subsingleton G] : IsZero G := by
   refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
   · ext x
     have : x = 1 := Subsingleton.elim _ _
-    rw [this, Hom.map_one, Hom.map_one]
+    rw [this, map_one, map_one]
   · ext
     apply Subsingleton.elim
 set_option linter.uppercaseLean3 false in
@@ -53,7 +53,7 @@ theorem isZero_of_subsingleton (G : CommGroupCat) [Subsingleton G] : IsZero G :=
   refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
   · ext x
     have : x = 1 := Subsingleton.elim _ _
-    rw [this, Hom.map_one, Hom.map_one]
+    rw [this, map_one, map_one]
   · ext
     apply Subsingleton.elim
 set_option linter.uppercaseLean3 false in
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
index 7722f4b1fa908..a1bad787fa49e 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -30,6 +30,8 @@ To construct an object in the category of `R`-modules from a type `M` with an in
 
 Similarly, there is a coercion from morphisms in `Module R` to linear maps.
 
+Porting note: the next two paragraphs should be revised.
+
 Unfortunately, Lean is not smart enough to see that, given an object `M : Module R`, the expression
 `of R M`, where we coerce `M` to the carrier type, is definitionally equal to `M` itself.
 This means that to go the other direction, i.e., from linear maps/equivalences to (iso)morphisms
@@ -85,7 +87,7 @@ namespace ModuleCat
 instance : CoeSort (ModuleCat.{v} R) (Type v) :=
   ⟨ModuleCat.carrier⟩
 
-attribute [-instance] Ring.toNonAssocRing
+attribute [coe] ModuleCat.carrier
 
 instance moduleCategory : Category (ModuleCat.{v} R) where
   Hom M N := M →ₗ[R] N
@@ -103,7 +105,7 @@ instance {M N : ModuleCat.{v} R} : FunLike (M ⟶ N) M (fun _ => N) :=
   ⟨fun f => f.toFun, fun _ _ h => LinearMap.ext (congr_fun h)⟩
 
 instance moduleConcreteCategory : ConcreteCategory.{v} (ModuleCat.{v} R) where
-  Forget :=
+  forget :=
     { obj := fun R => R
       map := fun f => f.toFun }
   forget_faithful := ⟨fun h => LinearMap.ext (fun x => by
@@ -114,13 +116,13 @@ set_option linter.uppercaseLean3 false in
 
 -- porting note: added to ease automation
 @[ext]
-lemma hom_ext {M N : ModuleCat.{v} R} (f₁ f₂ : M ⟶ N) (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
+lemma ext {M N : ModuleCat.{v} R} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
   FunLike.ext _ _ h
 
 instance hasForgetToAddCommGroup : HasForget₂ (ModuleCat R) AddCommGroupCat where
   forget₂ :=
     { obj := fun M => AddCommGroupCat.of M
-      map := fun f => LinearMap.toAddMonoidHom f }
+      map := fun f => AddCommGroupCat.ofHom f.toAddMonoidHom }
 set_option linter.uppercaseLean3 false in
 #align Module.has_forget_to_AddCommGroup ModuleCat.hasForgetToAddCommGroup
 
@@ -133,14 +135,18 @@ def of (X : Type v) [AddCommGroup X] [Module R X] : ModuleCat R :=
 set_option linter.uppercaseLean3 false in
 #align Module.of ModuleCat.of
 
--- porting note: remove simp attribute because it makes the linter complain
+@[simp]
 theorem forget₂_obj (X : ModuleCat R) :
     (forget₂ (ModuleCat R) AddCommGroupCat).obj X = AddCommGroupCat.of X :=
   rfl
 set_option linter.uppercaseLean3 false in
 #align Module.forget₂_obj ModuleCat.forget₂_obj
 
-@[simp 900]
+-- Porting note: the simpNF linter correctly doesn't like this.
+-- I'm not sure what this is for, actually.
+-- If it is really needed, better might be a simp lemma that says
+-- `AddCommGroupCat.of (ModuleCat.of R X) = AddCommGroupCat.of X`.
+-- @[simp 900]
 theorem forget₂_obj_moduleCat_of (X : Type v) [AddCommGroup X] [Module R X] :
     (forget₂ (ModuleCat R) AddCommGroupCat).obj (of R X) = AddCommGroupCat.of X :=
   rfl
@@ -154,6 +160,8 @@ theorem forget₂_map (X Y : ModuleCat R) (f : X ⟶ Y) :
 set_option linter.uppercaseLean3 false in
 #align Module.forget₂_map ModuleCat.forget₂_map
 
+-- Porting note: TODO: `ofHom` and `asHom` are duplicates!
+
 /-- Typecheck a `LinearMap` as a morphism in `Module R`. -/
 def ofHom {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y]
     [Module R Y] (f : X →ₗ[R] Y) : of R X ⟶ of R Y :=
@@ -265,8 +273,6 @@ scoped[ModuleCat] notation "↿" f:1024 => ModuleCat.asHomLeft f
 
 section
 
-attribute [-instance] Ring.toNonAssocRing
-
 /-- Build an isomorphism in the category `Module R` from a `LinearEquiv` between `Module`s. -/
 @[simps]
 def LinearEquiv.toModuleIso {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁}
diff --git a/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean b/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean
index f7c63efa10df3..8f28a00908472 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean
@@ -39,9 +39,7 @@ def ringEquivEndForget₂ (R : Type u) [Ring R] :
   invFun φ := φ.app (ModuleCat.of R R) (1 : R)
   left_inv := by
     intro r
-    dsimp
-    erw [AddCommGroupCat.ofHom_apply]
-    simp only [DistribMulAction.toAddMonoidHom_apply, smul_eq_mul, mul_one]
+    simp
   right_inv := by
     intro φ
     apply NatTrans.ext
diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean
index 637e6a46f2789..59907b5fe2baa 100644
--- a/Mathlib/Algebra/Category/MonCat/Basic.lean
+++ b/Mathlib/Algebra/Category/MonCat/Basic.lean
@@ -66,19 +66,39 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddMon.bundled_hom AddMonCat.bundledHom
 
-instance largeCategory : LargeCategory MonCat := by
-  dsimp only [MonCat]
-  infer_instance
+deriving instance LargeCategory for MonCat
+attribute [to_additive instAddMonCatLargeCategory] instMonCatLargeCategory
 
+@[to_additive]
 instance concreteCategory : ConcreteCategory MonCat :=
   BundledHom.concreteCategory _
 
-attribute [to_additive] MonCat.largeCategory MonCat.concreteCategory
+@[to_additive]
+instance : CoeSort MonCat (Type _) where
+  coe X := X.α
 
 @[to_additive]
-instance : CoeSort MonCat (Type _) := by
-  dsimp only [MonCat]
-  infer_instance
+instance (X : MonCat) : Monoid X := X.str
+
+-- porting note: this instance was not necessary in mathlib
+@[to_additive]
+instance {X Y : MonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
+  coe (f : X →* Y) := f
+
+-- porting note: added
+@[to_additive (attr := simp)]
+lemma coe_id {X : MonCat} : (𝟙 X : X → X) = id := rfl
+
+-- porting note: added
+@[to_additive (attr := simp)]
+lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
+
+-- porting note: added
+@[simp] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl
+
+@[to_additive (attr := ext)]
+lemma ext {X Y : MonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
+  MonoidHom.ext w
 
 /-- Construct a bundled `MonCat` from the underlying type and typeclass. -/
 @[to_additive]
@@ -89,33 +109,18 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddMon.of AddMonCat.of
 
-/-- Construct a bundled `MonCat` from the underlying type and typeclass. -/
+/-- Construct a bundled `AddMonCat` from the underlying type and typeclass. -/
 add_decl_doc AddMonCat.of
 
-/-- Typecheck a `MonoidHom` as a morphism in `MonCat`. -/
+-- Porting note: removed `@[simp]` here, as it makes it harder to tell when to apply
+-- bundled or unbundled lemmas.
+-- (This change seems dangerous!)
 @[to_additive]
-def ofHom {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : of X ⟶ of Y :=
-  f
-set_option linter.uppercaseLean3 false in
-#align Mon.of_hom MonCat.ofHom
+theorem coe_of (R : Type u) [Monoid R] : (MonCat.of R : Type u) = R := rfl
 set_option linter.uppercaseLean3 false in
-#align AddMon.of_hom AddMonCat.ofHom
-
-/-- Typecheck a `AddMonoidHom` as a morphism in `AddMonCat`. -/
-add_decl_doc AddMonCat.ofHom
-
--- porting note: this instance was not necessary in mathlib
-@[to_additive]
-instance {X Y : MonCat} : CoeFun (X ⟶ Y) fun _ => X → Y :=
-  ConcreteCategory.hasCoeToFun
-
--- porting note: in mathlib the LHS was `(⇑ofHom f) x`; the coercion was unfolded
--- to make the simp lemma work
-@[to_additive (attr := simp) _root_.AddMonCat.ofHom_apply]
-lemma ofHom_apply {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) (x : X) :
-  ((forget MonCat).map (MonCat.ofHom f)) x = f x := rfl
+#align Mon.coe_of MonCat.coe_of
 set_option linter.uppercaseLean3 false in
-#align Mon.of_hom_apply MonCat.ofHom_apply
+#align AddMon.coe_of AddMonCat.coe_of
 
 @[to_additive]
 instance : Inhabited MonCat :=
@@ -123,41 +128,25 @@ instance : Inhabited MonCat :=
   ⟨@of PUnit (@DivInvMonoid.toMonoid _ (@Group.toDivInvMonoid _
     (@CommGroup.toGroup _ PUnit.commGroup)))⟩
 
+/-- Typecheck a `MonoidHom` as a morphism in `MonCat`. -/
 @[to_additive]
-instance (M : MonCat) : Monoid M :=
-  M.str
-
-@[to_additive (attr := simp)]
-theorem coe_of (R : Type u) [Monoid R] : (MonCat.of R : Type u) = R :=
-  rfl
+def ofHom {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) : of X ⟶ of Y := f
 set_option linter.uppercaseLean3 false in
-#align Mon.coe_of MonCat.coe_of
+#align Mon.of_hom MonCat.ofHom
 set_option linter.uppercaseLean3 false in
-#align AddMon.coe_of AddMonCat.coe_of
-
-@[to_additive]
-instance {G : Type _} [Group G] : Group (MonCat.of G) := by assumption
-
--- porting note: this was added to ease the port
-/-- the morphism in `MonCat` associated to a `MonoidHom` -/
-@[to_additive (attr := simp)]
-def Hom.mk {X Y : MonCat} (f : X →* Y) : X ⟶ Y := f
+#align AddMon.of_hom AddMonCat.ofHom
 
-/-- the morphism in `AddMonCat` associated to a `AddMonoidHom` -/
-add_decl_doc AddMonCat.Hom.mk
+/-- Typecheck a `AddMonoidHom` as a morphism in `AddMonCat`. -/
+add_decl_doc AddMonCat.ofHom
 
--- porting note: this lemma was added to make automation work in `MonCat.forget_reflects_isos`
 @[to_additive (attr := simp)]
-lemma Hom.map_mul {X Y : MonCat} (f : X ⟶ Y) (x y : X) :
-  ((forget MonCat).map f) (x * y) =
-    f x * f y := by
-  apply MonoidHom.map_mul (show MonoidHom X Y from f)
+lemma ofHom_apply {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) (x : X) :
+  (ofHom f) x = f x := rfl
+set_option linter.uppercaseLean3 false in
+#align Mon.of_hom_apply MonCat.ofHom_apply
 
--- porting note: added as a complement to `Hom.map_mul`
-@[to_additive (attr := simp)]
-lemma Hom.map_one {X Y : MonCat} (f : X ⟶ Y) :
-  ((forget MonCat).map f) (1 : X) = (1 : Y) := by
-  apply MonoidHom.map_one (show MonoidHom X Y from f)
+@[to_additive]
+instance {G : Type _} [Group G] : Group (MonCat.of G) := by assumption
 
 end MonCat
 
@@ -178,20 +167,43 @@ namespace CommMonCat
 @[to_additive]
 instance : BundledHom.ParentProjection @CommMonoid.toMonoid := ⟨⟩
 
-instance largeCategory : LargeCategory CommMonCat := by
-  dsimp only [CommMonCat]
-  infer_instance
+deriving instance LargeCategory for CommMonCat
+attribute [to_additive instAddCommMonCatLargeCategory] instCommMonCatLargeCategory
 
+@[to_additive]
 instance concreteCategory : ConcreteCategory CommMonCat := by
   dsimp only [CommMonCat]
   infer_instance
 
-attribute [to_additive] CommMonCat.largeCategory CommMonCat.concreteCategory
+@[to_additive]
+instance : CoeSort CommMonCat (Type _) where
+  coe X := X.α
 
 @[to_additive]
-instance : CoeSort CommMonCat (Type _) := by
-  dsimp only [CommMonCat]
-  infer_instance
+instance (X : CommMonCat) : CommMonoid X := X.str
+
+-- porting note: this instance was not necessary in mathlib
+@[to_additive]
+instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
+  coe (f : X →* Y) := f
+
+-- porting note: added
+@[to_additive (attr := simp)]
+lemma coe_id {X : CommMonCat} : (𝟙 X : X → X) = id := rfl
+
+-- porting note: added
+@[to_additive (attr := simp)]
+lemma coe_comp {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
+
+-- porting note: added
+@[to_additive (attr := simp)]
+lemma forget_map {X Y : CommMonCat} (f : X ⟶ Y) :
+    (forget CommMonCat).map f = (f : X → Y) :=
+  rfl
+
+@[to_additive (attr := ext)]
+lemma ext {X Y : CommMonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
+  MonoidHom.ext w
 
 /-- Construct a bundled `CommMonCat` from the underlying type and typeclass. -/
 @[to_additive]
@@ -210,11 +222,10 @@ instance : Inhabited CommMonCat :=
   -- The default instance for `CommMonoid PUnit` is derived via `CommRing` which breaks to_additive
   ⟨@of PUnit (@CommGroup.toCommMonoid _ PUnit.commGroup)⟩
 
+-- Porting note: removed `@[simp]` here, as it makes it harder to tell when to apply
+-- bundled or unbundled lemmas.
+-- (This change seems dangerous!)
 @[to_additive]
-instance (M : CommMonCat) : CommMonoid M :=
-  M.str
-
-@[to_additive (attr := simp)]
 theorem coe_of (R : Type u) [CommMonoid R] : (CommMonCat.of R : Type u) = R :=
   rfl
 set_option linter.uppercaseLean3 false in
@@ -233,72 +244,44 @@ set_option linter.uppercaseLean3 false in
 @[to_additive]
 instance : Coe CommMonCat.{u} MonCat.{u} where coe := (forget₂ CommMonCat MonCat).obj
 
--- porting note: this instance was not necessary in mathlib
-@[to_additive]
-instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y :=
-  ConcreteCategory.hasCoeToFun
-
--- porting note: this was added to make automation work
+-- porting note: this was added to make automation work (it already exists for MonCat)
 /-- Typecheck a `MonoidHom` as a morphism in `CommMonCat`. -/
 @[to_additive]
-def ofHom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) : of X ⟶ of Y :=
-  f
+def ofHom {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) : of X ⟶ of Y := f
 
 /-- Typecheck a `AddMonoidHom` as a morphism in `AddCommMonCat`. -/
 add_decl_doc AddCommMonCat.ofHom
 
--- porting note: this was added to make automation work in `MulEquiv.toCommMonCatIso`
-@[to_additive (attr := simp) _root_.AddCommMonCat.ofHom_apply]
-lemma ofHom_apply {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) (x : X) :
-  ((forget CommMonCat).map (CommMonCat.ofHom f)) x = f x := rfl
-
--- porting note: this was added to make the following examples work
-/-- the morphism in `CommMonCat` associated to a `MonoidHom` -/
-@[to_additive (attr := simp)]
-def Hom.mk {X Y : CommMonCat} (f : X →* Y) : X ⟶ Y := f
-
-/-- the morphism in `AddCommMonCat` associated to a `AddMonoidHom` -/
-add_decl_doc AddCommMonCat.Hom.mk
-
--- porting note: this lemma was added to make automation work in `CommMonCat.forget_reflects_isos`
-@[to_additive (attr := simp)]
-lemma Hom.map_mul {X Y : CommMonCat} (f : X ⟶ Y) (x y : X) :
-  ((forget CommMonCat).map f) (x * y) = f x * f y := by
-  apply MonoidHom.map_mul (show MonoidHom X Y from f)
-
--- porting note: added as a complement to `Hom.map_mul`
 @[to_additive (attr := simp)]
-lemma Hom.map_one {X Y : CommMonCat} (f : X ⟶ Y) :
-  ((forget CommMonCat).map f) (1 : X) = (1 : Y) := by
-  apply MonoidHom.map_one (show MonoidHom X Y from f)
+lemma ofHom_apply {X Y : Type u} [CommMonoid X] [CommMonoid Y] (f : X →* Y) (x : X) :
+  (ofHom f) x = f x := rfl
 
 end CommMonCat
 
 -- We verify that the coercions of morphisms to functions work correctly:
 example {R S : MonCat} (f : R ⟶ S) : ↑R → ↑S := f
 
+-- Porting note: it's essential that simp lemmas for `→*` apply to morphisms.
+example {R S : MonCat} (i : R ⟶ S) (r : R) (h : r = 1) : i r = 1 := by simp [h]
+
 example {R S : CommMonCat} (f : R ⟶ S) : ↑R → ↑S := f
 
+example {R S : CommMonCat} (i : R ⟶ S) (r : R) (h : r = 1) : i r = 1 := by simp [h]
+
 -- We verify that when constructing a morphism in `CommMonCat`,
--- when we construct the `toFun` field, the types are presented as `↥R`,
--- rather than `R.α` or (as we used to have) `↥(bundled.map comm_monoid.to_monoid R)`.
+-- when we construct the `toFun` field, the types are presented as `↑R`.
 example (R : CommMonCat.{u}) : R ⟶ R :=
-  -- porting note: the constructor `CommMonCat.Hom.mk` was added to make this example work
-  CommMonCat.Hom.mk
-    { toFun := fun x => by
-        match_target (R : Type u)
-        -- porting note: is there an equivalent of `match_hyp` in Lean4?
-        --match_hyp x : (R : Type u)
-        exact x * x
-      map_one' := by simp
-      map_mul' := fun x y => by
-        dsimp
-        rw [mul_assoc x y (x * y), ← mul_assoc y x y, mul_comm y x, mul_assoc, mul_assoc] }
+  { toFun := fun x => by
+      match_target (R : Type u)
+      guard_hyp x : (R : Type u)
+      exact x * x
+    map_one' := by simp
+    map_mul' := fun x y => by
+      dsimp
+      rw [mul_assoc x y (x * y), ← mul_assoc y x y, mul_comm y x, mul_assoc, mul_assoc] }
 
 variable {X Y : Type u}
 
-attribute [local ext] ConcreteCategory.hom_ext
-
 section
 
 variable [Monoid X] [Monoid Y]
@@ -408,7 +391,7 @@ instance CommMonCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommMonC
   reflects {X Y} f _ := by
     let i := asIso ((forget CommMonCat).map f)
     let e : X ≃* Y := MulEquiv.mk i.toEquiv
-    -- porting note: same remark as for `MonCat.forget_reflects_iso`
+      -- Porting FIXME: this would ideally be `by aesop`, as in `MonCat.forget_reflects_isos`
       (MonoidHom.map_mul (show MonoidHom X Y from f))
     exact IsIso.of_iso e.toCommMonCatIso
 set_option linter.uppercaseLean3 false in
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory.lean b/Mathlib/AlgebraicTopology/SimplexCategory.lean
index 41b0d2a242252..852eed1fb55a2 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory.lean
@@ -464,7 +464,7 @@ end Truncated
 section Concrete
 
 instance : ConcreteCategory.{0} SimplexCategory where
-  Forget :=
+  forget :=
     { obj := fun i => Fin (i.len + 1)
       map := fun f => f.toOrderHom }
   forget_faithful := ⟨fun h => by ext : 2 ; exact h⟩
diff --git a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
index 03b058af1814c..4fee537a00137 100644
--- a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
+++ b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean
@@ -31,7 +31,7 @@ attribute [local instance]
   CategoryTheory.ConcreteCategory.hasCoeToSort CategoryTheory.ConcreteCategory.hasCoeToFun
 
 -- porting note: added, should be moved
-instance (x : SimplexCategory) : Fintype (CategoryTheory.ConcreteCategory.Forget.obj x) := by
+instance (x : SimplexCategory) : Fintype (CategoryTheory.ConcreteCategory.forget.obj x) := by
   change (Fintype (Fin _))
   infer_instance
 
@@ -65,7 +65,7 @@ def toTopMap {x y : SimplexCategory} (f : x ⟶ y) : x.toTopObj → y.toTopObj :
       intro e he
       simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
       apply h
-      simp only [CategoryTheory.forget_obj_eq_coe, Finset.mem_univ, forall_true_left,
+      simp only [Finset.mem_univ, forall_true_left,
         ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
         Finset.mem_filter, true_and] at he
       rw [← he.1, he.2]⟩
@@ -115,7 +115,7 @@ def toTop : SimplexCategory ⥤ TopCat where
       intro e he
       simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
       apply h
-      simp only [CategoryTheory.forget_obj_eq_coe, Finset.mem_univ, forall_true_left,
+      simp only [Finset.mem_univ, forall_true_left,
         ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
         Finset.mem_filter, true_and] at he
       rw [← he.1, he.2]
diff --git a/Mathlib/CategoryTheory/Category/Bipointed.lean b/Mathlib/CategoryTheory/Category/Bipointed.lean
index e2259fa5fa7fe..b5dc338411047 100644
--- a/Mathlib/CategoryTheory/Category/Bipointed.lean
+++ b/Mathlib/CategoryTheory/Category/Bipointed.lean
@@ -95,7 +95,7 @@ instance largeCategory : LargeCategory Bipointed where
 #align Bipointed.large_category Bipointed.largeCategory
 
 instance concreteCategory : ConcreteCategory Bipointed where
-  Forget :=
+  forget :=
     { obj := Bipointed.X
       map := @Hom.toFun }
   forget_faithful := ⟨@Hom.ext⟩
diff --git a/Mathlib/CategoryTheory/Category/Pointed.lean b/Mathlib/CategoryTheory/Category/Pointed.lean
index 10b07b8fa8744..7c5606f856059 100644
--- a/Mathlib/CategoryTheory/Category/Pointed.lean
+++ b/Mathlib/CategoryTheory/Category/Pointed.lean
@@ -104,7 +104,7 @@ set_option linter.uppercaseLean3 false in
 #align Pointed.large_category Pointed.largeCategory
 
 instance concreteCategory : ConcreteCategory Pointed where
-  Forget :=
+  forget :=
     { obj := Pointed.X
       map := @Hom.toFun }
   forget_faithful := ⟨@Hom.ext⟩
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
index 3c7f38448e778..487ca1d331f1a 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -57,25 +57,25 @@ They are specified that order, to avoid unnecessary universe annotations.
 -/
 class ConcreteCategory (C : Type u) [Category.{v} C] where
   /-- We have a functor to Type -/
-  Forget : C ⥤ Type w -- Porting note: it has Type in the signature...
+  protected forget : C ⥤ Type w
   /-- That functor is faithful -/
-  [forget_faithful : Faithful Forget]
+  [forget_faithful : Faithful forget]
 #align category_theory.concrete_category CategoryTheory.ConcreteCategory
-#align category_theory.concrete_category.forget CategoryTheory.ConcreteCategory.Forget
+#align category_theory.concrete_category.forget CategoryTheory.ConcreteCategory.forget
 
-attribute [reducible] ConcreteCategory.Forget
+attribute [reducible] ConcreteCategory.forget
 attribute [instance] ConcreteCategory.forget_faithful
 
 /-- The forgetful functor from a concrete category to `Type u`. -/
 @[reducible]
 def forget (C : Type v) [Category C] [ConcreteCategory.{u} C] : C ⥤ Type u :=
-  ConcreteCategory.Forget
+  ConcreteCategory.forget
 #align category_theory.forget CategoryTheory.forget
 
 -- this is reducible because we want `forget (Type u)` to unfold to `𝟭 _`
 @[reducible]
 instance ConcreteCategory.types : ConcreteCategory (Type u) where
-  Forget := 𝟭 _
+  forget := 𝟭 _
 #align category_theory.concrete_category.types CategoryTheory.ConcreteCategory.types
 
 /-- Provide a coercion to `Type u` for a concrete category. This is not marked as an instance
@@ -88,7 +88,7 @@ instance : HasCoeToSort X := ConcreteCategory.hasCoeToSort X
 -/
 def ConcreteCategory.hasCoeToSort (C : Type v) [Category C] [ConcreteCategory C] :
     CoeSort C (Type u) where
-  coe := fun X => ConcreteCategory.Forget.obj X
+  coe := fun X => (forget C).obj X
 #align category_theory.concrete_category.has_coe_to_sort CategoryTheory.ConcreteCategory.hasCoeToSort
 
 section
@@ -97,9 +97,8 @@ attribute [local instance] ConcreteCategory.hasCoeToSort
 
 variable {C : Type v} [Category C] [ConcreteCategory.{w} C]
 
-@[simp]
-theorem forget_obj_eq_coe {X : C} : (forget C).obj X = X := rfl
-#align category_theory.forget_obj_eq_coe CategoryTheory.forget_obj_eq_coe
+-- Porting note: forget_obj_eq_coe has become a syntactic tautology.
+#noalign category_theory.forget_obj_eq_coe
 
 /-- Usually a bundled hom structure already has a coercion to function
 that works with different universes. So we don't use this as a global instance. -/
@@ -118,9 +117,8 @@ theorem ConcreteCategory.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x =
   exact w x
 #align category_theory.concrete_category.hom_ext CategoryTheory.ConcreteCategory.hom_ext
 
-@[simp, nolint synTaut] -- Porting note: synTaut is fine with CoeFun.coe explicitly on the RHS
-theorem forget_map_eq_coe {X Y : C} (f : X ⟶ Y) : (forget C).map f = f := rfl
-#align category_theory.forget_map_eq_coe CategoryTheory.forget_map_eq_coe
+-- Porting note: `forget_map_eq_coe` becomes a syntactic tautology.
+#noalign category_theory.forget_map_eq_coe
 
 /-- Analogue of `congr_fun h x`,
 when `h : f = g` is an equality between morphisms in a concrete category.
@@ -206,7 +204,7 @@ class HasForget₂ (C : Type v) (D : Type v') [Category C] [ConcreteCategory.{u}
   [ConcreteCategory.{u} D] where
   /-- A functor from `C` to `D` -/
   forget₂ : C ⥤ D
-  /-- It covers the `ConcreteCategory.Forget` for `C` and `D` -/
+  /-- It covers the `ConcreteCategory.forget` for `C` and `D` -/
   forget_comp : forget₂ ⋙ forget D = forget C := by aesop
 #align category_theory.has_forget₂ CategoryTheory.HasForget₂
 
@@ -243,7 +241,7 @@ instance forget₂_preservesEpimorphisms (C : Type v) (D : Type v') [Category C]
 
 instance InducedCategory.concreteCategory {C : Type v} {D : Type v'} [Category D]
     [ConcreteCategory D] (f : C → D) : ConcreteCategory (InducedCategory D f) where
-  Forget := inducedFunctor f ⋙ forget D
+  forget := inducedFunctor f ⋙ forget D
 #align category_theory.induced_category.concrete_category CategoryTheory.InducedCategory.concreteCategory
 
 instance InducedCategory.hasForget₂ {C : Type v} {D : Type v'} [Category D] [ConcreteCategory D]
@@ -254,7 +252,7 @@ instance InducedCategory.hasForget₂ {C : Type v} {D : Type v'} [Category D] [C
 
 instance FullSubcategory.concreteCategory {C : Type v} [Category C] [ConcreteCategory C]
     (Z : C → Prop) : ConcreteCategory (FullSubcategory Z) where
-  Forget := fullSubcategoryInclusion Z ⋙ forget C
+  forget := fullSubcategoryInclusion Z ⋙ forget C
 #align category_theory.full_subcategory.concrete_category CategoryTheory.FullSubcategoryₓ.concreteCategory
 
 instance FullSubcategory.hasForget₂ {C : Type v} [Category C] [ConcreteCategory C] (Z : C → Prop) :
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean b/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean
index d8e6f1571a04e..0f6ac2959d8b3 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean
@@ -10,6 +10,7 @@ Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather
 -/
 import Std.Tactic.Lint.Frontend
 import Std.Tactic.Lint.Misc
+import Std.Tactic.CoeExt
 import Mathlib.Mathport.Rename
 
 /-!
@@ -39,6 +40,8 @@ structure Bundled (c : Type u → Type v) : Type max (u + 1) v where
 
 namespace Bundled
 
+attribute [coe] α
+
 -- This is needed so that we can ask for an instance of `c α` below even though Lean doesn't know
 -- that `c α` is a typeclass.
 set_option checkBinderAnnotations false in
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean b/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean
index 1ed152d89b342..43df450e66710 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean
@@ -79,7 +79,7 @@ instance category : Category (Bundled c) := by
 /-- A category given by `BundledHom` is a concrete category. -/
 instance concreteCategory : ConcreteCategory.{u} (Bundled c)
     where
-  Forget :=
+  forget :=
     { obj := fun X => X
       map := @fun X Y f => 𝒞.toFun X.str Y.str f
       map_id := fun X => 𝒞.id_toFun X.str
diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean
index 277846c617ee2..9a7bcf416d828 100644
--- a/Mathlib/CategoryTheory/GradedObject.lean
+++ b/Mathlib/CategoryTheory/GradedObject.lean
@@ -239,7 +239,7 @@ variable (β : Type)
 variable (C : Type (u + 1)) [LargeCategory C] [ConcreteCategory C] [HasCoproducts.{0} C]
   [HasZeroMorphisms C]
 
-instance : ConcreteCategory (GradedObject β C) where Forget := total β C ⋙ forget C
+instance : ConcreteCategory (GradedObject β C) where forget := total β C ⋙ forget C
 
 instance : HasForget₂ (GradedObject β C) C where forget₂ := total β C
 
diff --git a/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean b/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean
index c2bfbe628ab6e..f94eaf9713ebb 100644
--- a/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean
@@ -59,11 +59,11 @@ structure, see `preadditiveYonedaObj`.
 def preadditiveYoneda : C ⥤ Cᵒᵖ ⥤ AddCommGroupCat.{v} where
   obj Y := preadditiveYonedaObj Y ⋙ forget₂ _ _
   map f :=
-    { app := fun X => AddCommGroupCat.Hom.mk
+    { app := fun X =>
         { toFun := fun g => g ≫ f
           map_zero' := Limits.zero_comp
           map_add' := fun g g' => add_comp _ _ _ _ _ _ }
-      naturality := fun X X' g => AddCommGroupCat.ext _ _ _ _ fun x => Category.assoc _ _ _ }
+      naturality := fun X X' g => AddCommGroupCat.ext fun x => Category.assoc _ _ _ }
   map_id _ := by ext ; dsimp ; simp
   map_comp f g := by ext ; dsimp ; simp
 #align category_theory.preadditive_yoneda CategoryTheory.preadditiveYoneda
@@ -88,12 +88,12 @@ structure, see `preadditiveCoyonedaObj`.
 def preadditiveCoyoneda : Cᵒᵖ ⥤ C ⥤ AddCommGroupCat.{v} where
   obj X := preadditiveCoyonedaObj X ⋙ forget₂ _ _
   map f :=
-    { app := fun Y => AddCommGroupCat.Hom.mk
+    { app := fun Y =>
         { toFun := fun g => f.unop ≫ g
           map_zero' := Limits.comp_zero
           map_add' := fun g g' => comp_add _ _ _ _ _ _ }
       naturality := fun Y Y' g =>
-        AddCommGroupCat.ext _ _ _ _ fun x => Eq.symm <| Category.assoc _ _ _ }
+        AddCommGroupCat.ext fun x => Eq.symm <| Category.assoc _ _ _ }
   map_id _ := by ext ; dsimp ; simp
   map_comp f g := by ext ; dsimp ; simp
 #align category_theory.preadditive_coyoneda CategoryTheory.preadditiveCoyoneda
diff --git a/Mathlib/Order/Category/NonemptyFinLinOrdCat.lean b/Mathlib/Order/Category/NonemptyFinLinOrdCat.lean
index d1891ff4d7cb9..69e0e9ad3caf4 100644
--- a/Mathlib/Order/Category/NonemptyFinLinOrdCat.lean
+++ b/Mathlib/Order/Category/NonemptyFinLinOrdCat.lean
@@ -184,7 +184,7 @@ theorem epi_iff_surjective {A B : NonemptyFinLinOrdCat.{u}} (f : A ⟶ B) :
       congr
       rw [← cancel_epi f]
       ext a
-      simp only [forget_obj_eq_coe, coe_of, FunctorToTypes.map_comp_apply]
+      simp only [coe_of, FunctorToTypes.map_comp_apply]
       simp only [forget_map_apply]
       split_ifs with h₁ h₂ h₂
       any_goals rfl
diff --git a/Mathlib/Tactic/Elementwise.lean b/Mathlib/Tactic/Elementwise.lean
index fc0e7bca2a2ad..f104ee4896e5f 100644
--- a/Mathlib/Tactic/Elementwise.lean
+++ b/Mathlib/Tactic/Elementwise.lean
@@ -43,7 +43,7 @@ section theorems
 theorem forget_hom_Type (α β : Type u) (f : α ⟶ β) : (forget (Type u)).map f = f := rfl
 
 theorem forall_congr_forget_Type (α : Type u) (p : α → Prop) :
-  (∀ (x : ConcreteCategory.Forget.obj α), p x) ↔ ∀ (x : α), p x := Iff.rfl
+  (∀ (x : (forget (Type u)).obj α), p x) ↔ ∀ (x : α), p x := Iff.rfl
 
 attribute [local instance] ConcreteCategory.hasCoeToFun ConcreteCategory.hasCoeToSort
 
diff --git a/Mathlib/Topology/Category/CompHaus/Projective.lean b/Mathlib/Topology/Category/CompHaus/Projective.lean
index 6735c9a4c2735..aa1efcded3825 100644
--- a/Mathlib/Topology/Category/CompHaus/Projective.lean
+++ b/Mathlib/Topology/Category/CompHaus/Projective.lean
@@ -50,7 +50,7 @@ instance projective_ultrafilter (X : Type _) : Projective (of <| Ultrafilter X)
     have hh : Continuous h := continuous_ultrafilter_extend _
     use ⟨h, hh⟩
     apply Faithful.map_injective (F := forget CompHaus)
-    simp only [Functor.map_comp, forget_map_eq_coe, ContinuousMap.coe_mk, coe_comp]
+    simp only [Functor.map_comp, ContinuousMap.coe_mk, coe_comp]
     convert denseRange_pure.equalizer (g.continuous.comp hh) f.continuous _
     -- Porting note: We need to get the coercions to functions under control.
     -- The next two lines should not be needed.
diff --git a/Mathlib/Topology/Category/Profinite/Projective.lean b/Mathlib/Topology/Category/Profinite/Projective.lean
index 20d1fed7f7740..f881ebc289038 100644
--- a/Mathlib/Topology/Category/Profinite/Projective.lean
+++ b/Mathlib/Topology/Category/Profinite/Projective.lean
@@ -47,7 +47,7 @@ instance projective_ultrafilter (X : Type u) : Projective (of <| Ultrafilter X)
     have hh : Continuous h := continuous_ultrafilter_extend _
     use ⟨h, hh⟩
     apply Faithful.map_injective (F := forget Profinite)
-    simp only [forget_map_eq_coe, ContinuousMap.coe_mk, coe_comp]
+    simp only [ContinuousMap.coe_mk, coe_comp]
     convert denseRange_pure.equalizer (g.continuous.comp hh) f.continuous _
      -- Porting note: same fix as in `Topology.Category.CompHaus.Projective`
     let g'' : ContinuousMap Y Z := g
diff --git a/Mathlib/Topology/Category/Top/Basic.lean b/Mathlib/Topology/Category/Top/Basic.lean
index 6f352f16caac9..5f3f34ab7b2ee 100644
--- a/Mathlib/Topology/Category/Top/Basic.lean
+++ b/Mathlib/Topology/Category/Top/Basic.lean
@@ -169,7 +169,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 theorem openEmbedding_iff_comp_isIso' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] :
     OpenEmbedding ((forget TopCat).map f ≫ (forget TopCat).map g) ↔ OpenEmbedding f := by
-  simp only [←forget_obj_eq_coe, ←Functor.map_comp]
+  simp only [←Functor.map_comp]
   exact openEmbedding_iff_comp_isIso f g
 
 -- Porting note: simpNF requested partially simped version below
@@ -186,7 +186,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 theorem openEmbedding_iff_isIso_comp' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
     OpenEmbedding ((forget TopCat).map f ≫ (forget TopCat).map g) ↔ OpenEmbedding g := by
-  simp only [←forget_obj_eq_coe, ←Functor.map_comp]
+  simp only [←Functor.map_comp]
   exact openEmbedding_iff_isIso_comp f g
 
 end TopCat