Test mk_concrete_category

Mathlib.lean

@@ -6986,6 +6986,7 @@ public import Mathlib.Tactic.CategoryTheory.Coherence.Normalize
 public import Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
 public import Mathlib.Tactic.CategoryTheory.Elementwise
 public import Mathlib.Tactic.CategoryTheory.IsoReassoc
+public import Mathlib.Tactic.CategoryTheory.MkConcreteCategory
 public import Mathlib.Tactic.CategoryTheory.Monoidal.Basic
 public import Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
 public import Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Mathlib/Algebra/Category/AlgCat/Basic.lean

@@ -192,7 +192,7 @@ set_option backward.isDefEq.respectTransparency false in
 def adj : free.{u} R ⊣ forget (AlgCat.{u} R) :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun _ _ =>
-        { toFun := fun f ↦ TypeCat.ofHom ((FreeAlgebra.lift _).symm f.hom)
+        { toFun := fun f ↦ ↾ ((FreeAlgebra.lift _).symm f.hom)
           invFun := fun f ↦ ofHom <| (FreeAlgebra.lift _) f
           left_inv := fun f ↦ by aesop
           right_inv := fun f ↦ by aesop } }
@@ -229,8 +229,8 @@ end CategoryTheory.Iso
 @[simps]
 def algEquivIsoAlgebraIso {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] :
     (X ≃ₐ[R] Y) ≅ (AlgCat.of R X ≅ AlgCat.of R Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toAlgebraIso)
-  inv := TypeCat.ofHom (fun i ↦ i.toAlgEquiv)
+  hom := ↾ (fun e ↦ e.toAlgebraIso)
+  inv := ↾ (fun i ↦ i.toAlgEquiv)
 
 instance AlgCat.forget_reflects_isos : (forget (AlgCat.{u} R)).ReflectsIsomorphisms where
   reflects {X Y} f _ := by

Mathlib/Algebra/Category/Grp/Adjunctions.lean

@@ -104,7 +104,7 @@ instance : (free.{u}).PreservesMonomorphisms where
         ((Types.initial_iff_empty X).2 hX).some).isZero.eq_of_tgt
     · have hf : Function.Injective f := by rwa [← mono_iff_injective]
       obtain ⟨g, hg⟩ := hf.hasLeftInverse
-      have : IsSplitMono f := IsSplitMono.mk' { retraction := TypeCat.ofHom g }
+      have : IsSplitMono f := IsSplitMono.mk' { retraction := ↾ g }
       infer_instance
 
 end AddCommGrpCat

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -544,8 +544,8 @@ end CategoryTheory.Iso
 in `GrpCat` -/
 @[to_additive]
 def mulEquivIsoGroupIso {X Y : GrpCat.{u}} : (X ≃* Y) ≅ (X ≅ Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toGrpIso)
-  inv := TypeCat.ofHom (fun i ↦ i.groupIsoToMulEquiv)
+  hom := ↾ (fun e ↦ e.toGrpIso)
+  inv := ↾ (fun i ↦ i.groupIsoToMulEquiv)
 
 /-- Additive equivalences between `AddGroup`s are the same
 as (isomorphic to) isomorphisms in `AddGrpCat`. -/
@@ -555,8 +555,8 @@ add_decl_doc addEquivIsoAddGroupIso
 in `CommGrpCat`. -/
 @[to_additive]
 def mulEquivIsoCommGroupIso {X Y : CommGrpCat.{u}} : (X ≃* Y) ≅ (X ≅ Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toCommGrpIso)
-  inv := TypeCat.ofHom (fun i ↦ i.commGroupIsoToMulEquiv)
+  hom := ↾ (fun e ↦ e.toCommGrpIso)
+  inv := ↾ (fun i ↦ i.commGroupIsoToMulEquiv)
 
 /-- Additive equivalences between `AddCommGroup`s are
 the same as (isomorphic to) isomorphisms in `AddCommGrpCat`. -/

Mathlib/Algebra/Category/Grp/Yoneda.lean

@@ -35,8 +35,8 @@ coyoneda embedding. -/]
 def CommGrpCat.coyonedaForget :
     coyoneda ⋙ (Functor.whiskeringRight _ _ _).obj (forget _) ≅ CategoryTheory.coyoneda :=
   dsimp% NatIso.ofComponents fun X ↦ NatIso.ofComponents fun Y ↦ {
-    hom := TypeCat.ofHom (fun f ↦ ofHom f),
-    inv := TypeCat.ofHom (fun f ↦ f.hom) }
+    hom := ↾ (fun f ↦ ofHom f),
+    inv := ↾ (fun f ↦ f.hom) }
 
 /-- The Hom bifunctor sending a type `X` and a commutative group `G` to the commutative group
 `X → G` with pointwise operations.

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -75,8 +75,8 @@ lemma free_map_apply {X Y : Type u} (f : X ⟶ Y) (x : X) :
 @[simps]
 def freeHomEquiv {X : Type u} {M : ModuleCat.{u} R} :
     ((free R).obj X ⟶ M) ≃ (X ⟶ M) where
-  toFun φ := TypeCat.ofHom (fun x ↦ φ (freeMk x))
-  invFun ψ := freeDesc (TypeCat.ofHom ψ)
+  toFun φ := ↾ (fun x ↦ φ (freeMk x))
+  invFun ψ := freeDesc (↾ ψ)
   left_inv _ := by ext; simp
   right_inv _ := by ext; simp
 

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -84,62 +84,28 @@ lemma coe_of (X : Type v) [Ring X] [Module R X] : (of R X : Type v) = X :=
 example (X : Type v) [Ring X] [Module R X] : (of R X : Type v) = X := by with_reducible rfl
 example (M : ModuleCat.{v} R) : of R M = M := by with_reducible rfl
 
-set_option backward.privateInPublic true in
 variable {R} in
-/-- The type of morphisms in `ModuleCat R`. -/
-@[ext]
-structure Hom (M N : ModuleCat.{v} R) where
-  private mk ::
-  /-- The underlying linear map. -/
-  hom' : M →ₗ[R] N
+mk_concrete_category (ModuleCat.{v} R) (· →ₗ[R] ·) (fun M ↦ .id (M := M)) (.comp · ·)
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
-instance moduleCategory : Category.{v, max (v + 1) u} (ModuleCat.{v} R) where
-  Hom M N := Hom M N
-  id _ := ⟨LinearMap.id⟩
-  comp f g := ⟨g.hom'.comp f.hom'⟩
+/--
+info: ModuleCat.Hom.hom.{v, u} {R : Type u} [Ring R] {X Y : ModuleCat R} (f : X.Hom Y) : ↑X →ₗ[R] ↑Y
+-/
+#guard_msgs in
+#check ModuleCat.Hom.hom
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
-instance : ConcreteCategory (ModuleCat.{v} R) (· →ₗ[R] ·) where
-  hom := Hom.hom'
-  ofHom := Hom.mk
+#check ModuleCat.hom_comp
+#check ModuleCat.ofHom
+#check ModuleCat.ofHom_hom
+#check ModuleCat.hom_ofHom
 
 section
 
 variable {R}
 
-/-- Turn a morphism in `ModuleCat` back into a `LinearMap`. -/
-abbrev Hom.hom {A B : ModuleCat.{v} R} (f : Hom A B) :=
-  ConcreteCategory.hom (C := ModuleCat R) f
-
-/-- Typecheck a `LinearMap` as a morphism in `ModuleCat`. -/
-abbrev ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y]
-    (f : X →ₗ[R] Y) : of R X ⟶ of R Y :=
-  ConcreteCategory.ofHom (C := ModuleCat R) f
-
-/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
-def Hom.Simps.hom (A B : ModuleCat.{v} R) (f : Hom A B) :=
-  f.hom
-
-initialize_simps_projections Hom (hom' → hom)
-
-/-!
-The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`.
--/
-
-@[simp]
-lemma hom_id {M : ModuleCat.{v} R} : (𝟙 M : M ⟶ M).hom = LinearMap.id := rfl
-
 /- Provided for rewriting. -/
 lemma id_apply (M : ModuleCat.{v} R) (x : M) :
     (𝟙 M : M ⟶ M) x = x := by simp
 
-@[simp]
-lemma hom_comp {M N O : ModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) :
-    (f ≫ g).hom = g.hom.comp f.hom := rfl
-
 /- Provided for rewriting. -/
 lemma comp_apply {M N O : ModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) (x : M) :
     (f ≫ g) x = g (f x) := by simp
@@ -148,53 +114,12 @@ lemma comp_apply {M N O : ModuleCat.{v} R} (f : M ⟶ N) (g : N ⟶ O) (x : M) :
 lemma hom_ext {M N : ModuleCat.{v} R} {f g : M ⟶ N} (hf : f.hom = g.hom) : f = g :=
   Hom.ext hf
 
-lemma hom_bijective {M N : ModuleCat.{v} R} :
-    Function.Bijective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) where
-  left f g h := by cases f; cases g; simpa using h
-  right f := ⟨⟨f⟩, rfl⟩
-
-/-- Convenience shortcut for `ModuleCat.hom_bijective.injective`. -/
-lemma hom_injective {M N : ModuleCat.{v} R} :
-    Function.Injective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) :=
-  hom_bijective.injective
-
-/-- Convenience shortcut for `ModuleCat.hom_bijective.surjective`. -/
-lemma hom_surjective {M N : ModuleCat.{v} R} :
-    Function.Surjective (Hom.hom : (M ⟶ N) → (M →ₗ[R] N)) :=
-  hom_bijective.surjective
-
-@[simp]
-lemma hom_ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y]
-    [Module R Y] (f : X →ₗ[R] Y) : (ofHom f).hom = f := rfl
-
-@[simp]
-lemma ofHom_hom {M N : ModuleCat.{v} R} (f : M ⟶ N) :
-    ofHom (Hom.hom f) = f := rfl
-
-@[simp]
-lemma ofHom_id {M : Type v} [AddCommGroup M] [Module R M] : ofHom LinearMap.id = 𝟙 (of R M) := rfl
-
-@[simp]
-lemma ofHom_comp {M N O : Type v} [AddCommGroup M] [AddCommGroup N] [AddCommGroup O] [Module R M]
-    [Module R N] [Module R O] (f : M →ₗ[R] N) (g : N →ₗ[R] O) :
-    ofHom (g.comp f) = ofHom f ≫ ofHom g :=
-  rfl
-
-/- Doesn't need to be `@[simp]` since `simp only` can solve this. -/
-lemma ofHom_apply {M N : Type v} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
-    (f : M →ₗ[R] N) (x : M) : ofHom f x = f x := rfl
-
 lemma inv_hom_apply {M N : ModuleCat.{v} R} (e : M ≅ N) (x : M) : e.inv (e.hom x) = x := by
   simp
 
 lemma hom_inv_apply {M N : ModuleCat.{v} R} (e : M ≅ N) (x : N) : e.hom (e.inv x) = x := by
   simp
 
-/-- `ModuleCat.Hom.hom` bundled as an `Equiv`. -/
-def homEquiv {M N : ModuleCat.{v} R} : (M ⟶ N) ≃ (M →ₗ[R] N) where
-  toFun := Hom.hom
-  invFun := ofHom
-
 set_option backward.privateInPublic true in
 set_option backward.privateInPublic.warn false in
 /-- The categorical equivalence between `ModuleCat` and `SemimoduleCat`.
@@ -299,8 +224,8 @@ in `ModuleCat` -/
 @[simps]
 def linearEquivIsoModuleIso {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X]
     [Module R Y] : (X ≃ₗ[R] Y) ≅ (ModuleCat.of R X ≅ ModuleCat.of R Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toModuleIso)
-  inv := TypeCat.ofHom (fun i ↦ i.toLinearEquiv)
+  hom := ↾ (fun e ↦ e.toModuleIso)
+  inv := ↾ (fun i ↦ i.toLinearEquiv)
 
 end
 
@@ -374,7 +299,9 @@ def homAddEquiv : (M ⟶ N) ≃+ (M →ₗ[R] N) :=
 
 theorem subsingleton_of_isZero (h : IsZero M) : Subsingleton M := by
   refine subsingleton_of_forall_eq 0 (fun x ↦ ?_)
-  rw [← LinearMap.id_apply (R := R) x, ← ModuleCat.hom_id]
+  have := ModuleCat.hom_id (R := R) (X := M)
+  dsimp only at this
+  rw [← LinearMap.id_apply (R := R) x, ← this]
   simp only [(CategoryTheory.Limits.IsZero.iff_id_eq_zero M).mp h, hom_zero, LinearMap.zero_apply]
 
 lemma isZero_iff_subsingleton : IsZero M ↔ Subsingleton M where
@@ -603,7 +530,8 @@ def ofHom₂ {M N P : ModuleCat.{u} R} (f : M →ₗ[R] N →ₗ[R] P) :
 /-- Turn a homomorphism into a bilinear map. -/
 @[simps!]
 def Hom.hom₂ {M N P : ModuleCat.{u} R} (f : M ⟶ (of R (N ⟶ P))) : M →ₗ[R] N →ₗ[R] P :=
-  (f ≫ ofHom homLinearEquiv.toLinearMap).hom
+  -- (f ≫ ofHom ((homLinearEquiv (M := N) (N := P)).toLinearMap)).hom
+  (f ≫ ofHom (X := of R (N ⟶ P)) (Y := of R (N →ₗ[R] P)) homLinearEquiv.toLinearMap).hom
 
 @[simp] lemma Hom.hom₂_ofHom₂ {M N P : ModuleCat.{u} R} (f : M →ₗ[R] N →ₗ[R] P) :
     (ofHom₂ f).hom₂ = f := rfl

Mathlib/Algebra/Category/ModuleCat/LeftResolution.lean

@@ -34,7 +34,7 @@ instance (X : Type u) : Projective ((free R).obj X) where
   factors {M N} f p hp := by
     rw [epi_iff_surjective] at hp
     obtain ⟨s, hs⟩ := hp.hasRightInverse
-    exact ⟨freeDesc (TypeCat.ofHom (fun x ↦ s (f (freeMk x)))), by cat_disch⟩
+    exact ⟨freeDesc (↾ (fun x ↦ s (f (freeMk x)))), by cat_disch⟩
 
 set_option backward.isDefEq.respectTransparency false in
 /-- An `R`-module `M` can be functorially written as a quotient of a

Mathlib/Algebra/Category/ModuleCat/Presheaf/ColimitFunctor.lean

@@ -79,7 +79,7 @@ by `cR.pt` on `ModuleColimit hcR hcM`. -/
 noncomputable def coconeSMul :
     Cocone (R ⋙ forget _ ⊗ M.presheaf ⋙ forget _) where
   pt := ModuleColimit hcR hcM
-  ι.app U := TypeCat.ofHom fun ⟨(r : R.obj U), (m : M.obj U)⟩ ↦ by exact cM.ι.app U (r • m)
+  ι.app U := ↾ fun ⟨(r : R.obj U), (m : M.obj U)⟩ ↦ by exact cM.ι.app U (r • m)
   ι.naturality V U f := by
     ext ⟨r, m⟩
     exact (ConcreteCategory.congr_arg (cM.ι.app U)

Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean

@@ -41,7 +41,7 @@ of modules over `R` which sends `X : Cᵒᵖ` to the free `R.obj X`-module on `F
 @[simps]
 noncomputable def freeObj (F : Cᵒᵖ ⥤ Type u) : PresheafOfModules.{u} R where
   obj X := (ModuleCat.free (R.obj X)).obj (F.obj X)
-  map {X Y} f := ModuleCat.freeDesc (TypeCat.ofHom (fun x ↦ ModuleCat.freeMk (F.map f x)))
+  map {X Y} f := ModuleCat.freeDesc (↾ (fun x ↦ ModuleCat.freeMk (F.map f x)))
   map_id := by aesop
 
 /-- The free presheaf of modules functor `(Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R`. -/
@@ -71,7 +71,7 @@ variable (F R) in
 /-- The unit of `PresheafOfModules.freeAdjunction`. -/
 @[simps]
 noncomputable def freeAdjunctionUnit : F ⟶ (freeObj (R := R) F).presheaf ⋙ forget _ where
-  app X := TypeCat.ofHom (fun x ↦ ModuleCat.freeMk x)
+  app X := ↾ (fun x ↦ ModuleCat.freeMk x)
   naturality X Y f := by ext; simp [presheaf]
 
 set_option backward.isDefEq.respectTransparency false in

Mathlib/Algebra/Category/ModuleCat/Semi.lean

@@ -273,8 +273,8 @@ in `SemimoduleCat` -/
 def linearEquivIsoModuleIsoₛ {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] [Module R X]
     [Module R Y] : (X ≃ₗ[R] Y) ≅
       ((SemimoduleCat.of R X) ≅ (SemimoduleCat.of R Y)) where
-  hom := TypeCat.ofHom (fun e ↦ e.toModuleIsoₛ)
-  inv := TypeCat.ofHom (fun i ↦ i.toLinearEquivₛ)
+  hom := ↾ (fun e ↦ e.toModuleIsoₛ)
+  inv := ↾ (fun i ↦ i.toLinearEquivₛ)
 
 end
 

Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

@@ -150,7 +150,7 @@ variable (R) in
 @[simps]
 def sectionsFunctor : SheafOfModules.{v} R ⥤ Type _ where
   obj M := M.sections
-  map f := TypeCat.ofHom (sectionsMap f)
+  map f := ↾ (sectionsMap f)
 
 variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
 

Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

@@ -158,14 +158,14 @@ noncomputable def freeSumIso : free I ⨿ free J ≅ free (R := R) (I ⊕ J) :=
 @[reassoc (attr := simp)]
 lemma inl_freeSumIso_hom :
     coprod.inl ≫ (freeSumIso (R := R) I J).hom = freeMap Sum.inl := by
-  rw [← dsimp% freeFunctor_map (TypeCat.ofHom (Sum.inl : I → I ⊕ J))]
+  rw [← dsimp% freeFunctor_map (↾ (Sum.inl : I → I ⊕ J))]
   exact IsColimit.comp_coconePointUniqueUpToIso_hom
     (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .left)
 
 @[reassoc (attr := simp)]
 lemma inr_freeSumIso_hom :
     coprod.inr ≫ (freeSumIso (R := R) I J).hom = freeMap Sum.inr := by
-  rw [← dsimp% freeFunctor_map (TypeCat.ofHom (Sum.inr : J → I ⊕ J))]
+  rw [← dsimp% freeFunctor_map (↾ (Sum.inr : J → I ⊕ J))]
   exact IsColimit.comp_coconePointUniqueUpToIso_hom
     (coprodIsCoprod (free (R := R) I) (free J)) _ (.mk .right)
 

Mathlib/Algebra/Category/MonCat/Adjunctions.lean

@@ -98,7 +98,7 @@ set_option backward.isDefEq.respectTransparency false in
 /-- The free-forgetful adjunction for commutative monoids. -/
 noncomputable
 def adj : free ⊣ forget AddCommMonCat.{u} where
-  unit := { app X := TypeCat.ofHom fun i ↦ Finsupp.single i 1 }
+  unit := { app X := ↾ fun i ↦ Finsupp.single i 1 }
   counit :=
   { app M := ofHom (Finsupp.liftAddHom (multiplesHom M))
     naturality {M N} f := by ext1; apply Finsupp.liftAddHom.symm.injective; cat_disch }

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -469,8 +469,8 @@ in `MonCat` -/
 @[to_additive addEquivIsoAddMonCatIso]
 def mulEquivIsoMonCatIso {X Y : Type u} [Monoid X] [Monoid Y] :
     (X ≃* Y) ≅ (MonCat.of X ≅ MonCat.of Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toMonCatIso)
-  inv := TypeCat.ofHom (fun i ↦ i.monCatIsoToMulEquiv)
+  hom := ↾ (fun e ↦ e.toMonCatIso)
+  inv := ↾ (fun i ↦ i.monCatIsoToMulEquiv)
 
 /-- additive equivalences between `AddMonoid`s are the same
 as (isomorphic to) isomorphisms in `AddMonCat` -/
@@ -481,8 +481,8 @@ in `CommMonCat` -/
 @[to_additive addEquivIsoAddCommMonCatIso]
 def mulEquivIsoCommMonCatIso {X Y : Type u} [CommMonoid X] [CommMonoid Y] :
     (X ≃* Y) ≅ (CommMonCat.of X ≅ CommMonCat.of Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toCommMonCatIso)
-  inv := TypeCat.ofHom (fun i ↦ i.commMonCatIsoToMulEquiv)
+  hom := ↾ (fun e ↦ e.toCommMonCatIso)
+  inv := ↾ (fun i ↦ i.commMonCatIsoToMulEquiv)
 
 /-- additive equivalences between `AddCommMonoid`s are
 the same as (isomorphic to) isomorphisms in `AddCommMonCat` -/

Mathlib/Algebra/Category/MonCat/Yoneda.lean

@@ -36,8 +36,8 @@ coyoneda embedding. -/]
 def CommMonCat.coyonedaForget :
     coyoneda ⋙ (Functor.whiskeringRight _ _ _).obj (forget _) ≅ CategoryTheory.coyoneda :=
   dsimp% NatIso.ofComponents fun X ↦ NatIso.ofComponents fun Y ↦ {
-    hom := TypeCat.ofHom (fun f ↦ ofHom f)
-    inv := TypeCat.ofHom (fun f ↦ f.hom) }
+    hom := ↾ (fun f ↦ ofHom f)
+    inv := ↾ (fun f ↦ f.hom) }
 
 /-- The Hom bifunctor sending a type `X` and a commutative monoid `M` to the commutative monoid
 `X → M` with pointwise operations.

Mathlib/Algebra/Category/Ring/Adjunctions.lean

@@ -51,7 +51,7 @@ set_option backward.isDefEq.respectTransparency false in
 def adj : free ⊣ forget CommRingCat.{u} :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun _ _ ↦
-        { toFun := fun f ↦ TypeCat.ofHom (homEquiv f.hom)
+        { toFun := fun f ↦ ↾ (homEquiv f.hom)
           invFun := fun f ↦ ofHom <| homEquiv.symm f
           left_inv := fun f ↦ congrArg ofHom (homEquiv.left_inv f.hom)
           right_inv := by cat_disch }
@@ -73,7 +73,7 @@ def coyoneda : Type vᵒᵖ ⥤ CommRingCat.{u} ⥤ CommRingCat.{max u v} where
 /-- The adjunction `Hom_{CRing}(Fun(n, R), S) ≃ Fun(n, Hom_{CRing}(R, S))`. -/
 def coyonedaAdj (R : CommRingCat.{u}) :
     (coyoneda.flip.obj R).rightOp ⊣ yoneda.obj R where
-  unit := { app n := TypeCat.ofHom (fun i ↦ CommRingCat.ofHom (Pi.evalRingHom _ i)) }
+  unit := { app n := ↾ (fun i ↦ CommRingCat.ofHom (Pi.evalRingHom _ i)) }
   counit := { app S := (CommRingCat.ofHom (Pi.ringHom fun f ↦ f.hom)).op }
 
 instance (R : CommRingCat.{u}) : (yoneda.obj R).IsRightAdjoint := ⟨_, ⟨coyonedaAdj R⟩⟩

Mathlib/Algebra/Category/Semigrp/Basic.lean

@@ -419,8 +419,8 @@ in `MagmaCat` -/
     as (isomorphic to) isomorphisms in `AddMagmaCat` -/]
 def mulEquivIsoMagmaIso {X Y : Type u} [Mul X] [Mul Y] :
     (X ≃* Y) ≅ (MagmaCat.of X ≅ MagmaCat.of Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toMagmaCatIso)
-  inv := TypeCat.ofHom (fun i ↦ i.magmaCatIsoToMulEquiv)
+  hom := ↾ (fun e ↦ e.toMagmaCatIso)
+  inv := ↾ (fun i ↦ i.magmaCatIsoToMulEquiv)
 
 /-- multiplicative equivalences between `Semigroup`s are the same as (isomorphic to) isomorphisms
 in `Semigroup` -/
@@ -429,8 +429,8 @@ in `Semigroup` -/
   the same as (isomorphic to) isomorphisms in `AddSemigroup` -/]
 def mulEquivIsoSemigrpIso {X Y : Type u} [Semigroup X] [Semigroup Y] :
     (X ≃* Y) ≅ (Semigrp.of X ≅ Semigrp.of Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toSemigrpIso)
-  inv := TypeCat.ofHom (fun i ↦ i.semigrpIsoToMulEquiv)
+  hom := ↾ (fun e ↦ e.toSemigrpIso)
+  inv := ↾ (fun i ↦ i.semigrpIsoToMulEquiv)
 
 @[to_additive]
 instance MagmaCat.forgetReflectsIsos : (forget MagmaCat.{u}).ReflectsIsomorphisms where