cleanup

dagurtomas · dagurtomas · commit fae92dbf6f7f · 2026-04-11T23:14:21.000-06:00
diff --git a/Mathlib/Algebra/Category/AlgCat/Basic.lean b/Mathlib/Algebra/Category/AlgCat/Basic.lean
@@ -150,7 +150,7 @@ instance : Inhabited (AlgCat R) :=
 
 lemma forget_obj {A : AlgCat.{v} R} : (forget (AlgCat.{v} R)).obj A = A := rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_coe (since := "2026-03-03")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-03")]
 lemma forget_map {A B : AlgCat.{v} R} (f : A ⟶ B) :
     (forget (AlgCat.{v} R)).map f = (f : _ → _) :=
   rfl
diff --git a/Mathlib/Algebra/Category/CommAlgCat/Basic.lean b/Mathlib/Algebra/Category/CommAlgCat/Basic.lean
@@ -122,7 +122,7 @@ instance : Inhabited (CommAlgCat R) := ⟨of R R⟩
 
 lemma forget_obj (A : CommAlgCat.{v} R) : (forget (CommAlgCat.{v} R)).obj A = A := rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_coe (since := "2026-03-06")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-06")]
 lemma forget_map (f : A ⟶ B) : (forget (CommAlgCat.{v} R)).map f = (f : _ → _) := rfl
 
 instance : CommRing ((forget (CommAlgCat R)).obj A) := inferInstanceAs <| CommRing A
diff --git a/Mathlib/Algebra/Category/CommBialgCat.lean b/Mathlib/Algebra/Category/CommBialgCat.lean
@@ -123,7 +123,7 @@ instance : Inhabited (CommBialgCat R) := ⟨of R R⟩
 lemma forget_obj (A : CommBialgCat.{v} R) : (forget (CommBialgCat.{v} R)).obj A = A :=
   rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_coe (since := "2026-03-06")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-06")]
 lemma forget_map (f : A ⟶ B) : (forget (CommBialgCat.{v} R)).map f = (f : _ → _) := rfl
 
 instance : CommRing ((forget (CommBialgCat R)).obj A) := inferInstanceAs <| CommRing A
diff --git a/Mathlib/Algebra/Category/Grp/Basic.lean b/Mathlib/Algebra/Category/Grp/Basic.lean
@@ -120,7 +120,7 @@ lemma coe_id {X : GrpCat} : (𝟙 X : X → X) = id := rfl
 @[to_additive (attr := simp)]
 lemma coe_comp {X Y Z : GrpCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
-@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 @[to_additive (attr := ext)]
 lemma ext {X Y : GrpCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
@@ -337,7 +337,7 @@ lemma coe_id {X : CommGrpCat} : (𝟙 X : X → X) = id := rfl
 @[to_additive (attr := simp)]
 lemma coe_comp {X Y Z : CommGrpCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
-@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 @[to_additive (attr := ext)]
 lemma ext {X Y : CommGrpCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -74,7 +74,6 @@ noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrpCat.{v}) :
 open scoped MonObj
 
 set_option backward.isDefEq.respectTransparency false in
--- attribute [local simp] types_tensorObj_def types_tensorUnit_def in
 attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp in
 /-- Implementation, see `leftExactFunctorForgetEquivalence`.
 This is the complicated bit, where we show that forgetting the group structure in the image of
@@ -88,7 +87,7 @@ noncomputable def unitIsoAux (F : C ⥤ AddCommGrpCat.{v}) [PreservesFiniteLimit
   refine CommGrp.mkIso Multiplicative.toAdd.toIso (by
     erw [Functor.mapCommGrp_obj_grp_one]
     cat_disch) ?_
-  dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_coe]
+  dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_ofHom]
   have : F.Additive := Functor.additive_of_preserves_binary_products _
   simp only [Category.id_comp]
   erw [Functor.mapCommGrp_obj_grp_mul]
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -217,7 +217,7 @@ end
 definitional equality issues. -/
 lemma forget_obj {M : ModuleCat.{v} R} : (forget (ModuleCat.{v} R)).obj M = M := rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_coe (since := "2026-03-02")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-03-02")]
 lemma forget_map {M N : ModuleCat.{v} R} (f : M ⟶ N) :
     (forget (ModuleCat.{v} R)).map f = (f : _ → _) :=
   rfl
diff --git a/Mathlib/Algebra/Category/ModuleCat/Semi.lean b/Mathlib/Algebra/Category/ModuleCat/Semi.lean
@@ -195,7 +195,7 @@ definitional equality issues. -/
 lemma forget_obj {M : SemimoduleCat.{v} R} : ((forget (SemimoduleCat.{v} R)).obj M : Type _) = M :=
   rfl
 
-@[deprecated ConcreteCategory.forget_map_eq_coe (since := "2026-02-25")]
+@[deprecated ConcreteCategory.forget_map_eq_ofHom (since := "2026-02-25")]
 lemma forget_map {M N : SemimoduleCat.{v} R} (f : M ⟶ N) :
     (forget (SemimoduleCat.{v} R)).map f = (f : _ → _) :=
   rfl
diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean
@@ -309,7 +309,7 @@ lemma coe_id {X : CommMonCat} : (𝟙 X : X → X) = id := rfl
 @[to_additive (attr := simp)]
 lemma coe_comp {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
-@[deprecated (since := "2026-02-15")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-15")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 @[to_additive (attr := ext)]
 lemma ext {X Y : CommMonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean
@@ -156,7 +156,7 @@ unif_hint forget_obj_eq_coe (R R' : SemiRingCat) where
   (forget SemiRingCat).obj R ≟ SemiRingCat.carrier R'
 
 @[deprecated (since := "2026-02-16")] alias forget_obj := CategoryTheory.forget_obj
-@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 instance {R : SemiRingCat} : Semiring ((forget SemiRingCat).obj R) :=
   inferInstanceAs <| Semiring R.carrier
@@ -326,7 +326,7 @@ unif_hint forget_obj_eq_coe (R R' : RingCat) where
   (forget RingCat).obj R ≟ RingCat.carrier R'
 
 @[deprecated (since := "2026-02-16")] alias forget_obj := CategoryTheory.forget_obj
-@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 instance {R : RingCat} : Ring ((forget RingCat).obj R) :=
   inferInstanceAs <| Ring R.carrier
@@ -498,7 +498,7 @@ unif_hint forget_obj_eq_coe (R R' : CommSemiRingCat) where
   (forget CommSemiRingCat).obj R ≟ CommSemiRingCat.carrier R'
 
 @[deprecated (since := "2026-02-16")] alias forget_obj := CategoryTheory.forget_obj
-@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 instance {R : CommSemiRingCat} : CommSemiring ((forget CommSemiRingCat).obj R) :=
   inferInstanceAs <| CommSemiring R.carrier
@@ -665,7 +665,7 @@ instance : Inhabited CommRingCat :=
   ⟨of PUnit⟩
 
 @[deprecated (since := "2026-02-16")] alias forget_obj := CategoryTheory.forget_obj
-@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-16")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 /-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.
 
diff --git a/Mathlib/Algebra/Category/Semigrp/Basic.lean b/Mathlib/Algebra/Category/Semigrp/Basic.lean
@@ -128,7 +128,7 @@ lemma coe_id {X : MagmaCat} : (𝟙 X : X → X) = id := rfl
 @[to_additive (attr := simp)]
 lemma coe_comp {X Y Z : MagmaCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
-@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 @[to_additive (attr := ext)]
 lemma ext {X Y : MagmaCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
@@ -290,7 +290,7 @@ lemma coe_id {X : Semigrp} : (𝟙 X : X → X) = id := rfl
 @[to_additive (attr := simp)]
 lemma coe_comp {X Y Z : Semigrp} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
-@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_coe
+@[deprecated (since := "2026-02-10")] alias forget_map := ConcreteCategory.forget_map_eq_ofHom
 
 @[to_additive (attr := ext)]
 lemma ext {X Y : Semigrp} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
diff --git a/Mathlib/AlgebraicTopology/SimplicialNerve.lean b/Mathlib/AlgebraicTopology/SimplicialNerve.lean
@@ -118,7 +118,7 @@ def compFunctor {J : Type*} [LinearOrder J]
 
 attribute [local ext (iff := false)] Functor.ext in
 attribute [local simp] types_tensorObj_def in
-@[simps] -- consider making these lemmas `-isSimp` and just local `simp` in this file
+@[simps -isSimp]
 instance (J : Type*) [LinearOrder J] :
     SimplicialCategory (SimplicialThickening J) where
   Hom i j := nerve (i ⟶ j)
@@ -127,16 +127,20 @@ instance (J : Type*) [LinearOrder J] :
     fun _ _ _ ↦ by simp; rfl⟩
   homEquiv {i j} := nerveEquiv.symm.trans (SSet.unitHomEquiv (nerve (i ⟶ j))).symm
 
+attribute [local simp] SimplicialThickening.Hom_def
+
 /-- Auxiliary definition for `SimplicialThickening.functor` -/
-@[simps]
-def functorMap {J K : Type u} [LinearOrder J] [LinearOrder K]
+abbrev functorMap {J K : Type u} [LinearOrder J] [LinearOrder K]
     (f : J →o K) (i j : SimplicialThickening J) :
       (i ⟶ j) ⥤ ((SimplicialThickening.mk <| f i.as) ⟶ (SimplicialThickening.mk <| f j.as)) where
   obj I := ⟨f '' I.I, Set.mem_image_of_mem f I.left, Set.mem_image_of_mem f I.right,
     by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.left_le k hk),
     by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.le_right k hk)⟩
   map f := ⟨⟨⟨Set.image_mono f.1.1.1⟩⟩⟩
 
+@[deprecated "No replacement, was using a bad instance" (since := "01-12-2026")]
+alias orderHom := functorMap
+
 attribute [local simp] nerveMap_app
 
 attribute [local simp] types_tensorObj_def in
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean
@@ -132,9 +132,7 @@ lemma finite_iSup_iff {X : SSet.{u}} {ι : Type*} [Finite ι]
       (by simpa only [nonDegenerate_iff_of_mono] using s.nonDegenerate)) ?_
   intro s
   obtain ⟨d, ⟨⟨s, h₁⟩, h₂⟩, rfl⟩ := s.mk_surjective
-  simp only [Subfunctor.iSup_obj] at h₁
-  change s ∈ (⋃ (i : ι), (A i).obj (Opposite.op ⦋d⦌)) at h₁
-  rw [Set.mem_iUnion] at h₁
+  simp only [Subfunctor.iSup_obj, Set.mem_iUnion] at h₁
   obtain ⟨i, hi⟩ := h₁
   rw [Subcomplex.mem_nonDegenerate_iff] at h₂
   exact ⟨⟨i, N.mk ⟨s, hi⟩ (by rwa [Subcomplex.mem_nonDegenerate_iff])⟩, rfl⟩
diff --git a/Mathlib/CategoryTheory/Action/Concrete.lean b/Mathlib/CategoryTheory/Action/Concrete.lean
@@ -90,10 +90,8 @@ def ofMulActionLimitCone {ι : Type v} (G : Type max v u) [Monoid G] (F : ι →
       uniq := fun s f h => by
         ext x
         funext j
-        simp only [Discrete.functor_obj_eq_as, Functor.const_obj_obj, Discrete.natTrans_app,
-          Discrete.forall, TypeCat.Fun.toFun_apply, ConcreteCategory.hom_ofHom,
-          TypeCat.Fun.coe_mk] at *
-        rw [← h j]
+        dsimp at *
+        rw [← h ⟨j⟩]
         rfl }
 
 /-- The `G`-set `G`, acting on itself by left multiplication. -/
diff --git a/Mathlib/CategoryTheory/Adhesive/Basic.lean b/Mathlib/CategoryTheory/Adhesive/Basic.lean
@@ -419,7 +419,7 @@ instance Adhesive.desc_mono_of_mono [Adhesive C] {Z A B : C}
           ← sq_f_v.w_assoc, w, ← pullback.condition_assoc, Category.assoc,
           ← sq_g_v.w_assoc]
 
-instance TypeCat.adhesive : Adhesive (Type u) :=
+instance Type.adhesive : Adhesive (Type u) :=
   ⟨fun {_ _ _ _ f _ _ _ _} H =>
     (IsPushout.isVanKampen_inl _ (Types.isCoprodOfMono f) _ _ _ H.flip).flip⟩
 
diff --git a/Mathlib/CategoryTheory/Adjunction/Opposites.lean b/Mathlib/CategoryTheory/Adjunction/Opposites.lean
@@ -78,14 +78,12 @@ set_option backward.isDefEq.respectTransparency false in
 `F.op ⋙ coyoneda ≅ F'.op ⋙ coyoneda`.
 We use this in combination with `fullyFaithfulCancelRight` to show left adjoints are unique.
 -/
-@[deprecated "No replacement." (since := "2026-03-03")]
 def leftAdjointsCoyonedaEquiv {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
     F.op ⋙ coyoneda ≅ F'.op ⋙ coyoneda :=
-  NatIso.ofComponents (fun X =>
-    (NatIso.ofComponents (fun Y =>
-      ((adj1.homEquiv X.unop Y).trans (adj2.homEquiv X.unop Y).symm).toIso) (by cat_disch)))
+  NatIso.ofComponents fun X =>
+    NatIso.ofComponents fun Y =>
+      ((adj1.homEquiv X.unop Y).trans (adj2.homEquiv X.unop Y).symm).toIso
 
-set_option linter.deprecated false in
 /-- Deprecated: prefer `(Adjunction.conjugateIsoEquiv adj1 adj2).symm`. -/
 @[deprecated "Use `(Adjunction.conjugateIsoEquiv adj1 adj2).symm` \
   (requires `import Mathlib.CategoryTheory.Adjunction.Mates`)." (since := "2026-01-31")]
diff --git a/Mathlib/CategoryTheory/Category/PartialFun.lean b/Mathlib/CategoryTheory/Category/PartialFun.lean
@@ -137,13 +137,12 @@ noncomputable def partialFunEquivPointed : PartialFun.{u} ≌ Pointed where
           · exact (hb rfl).elim
           · simp only [partialFunToPointed_obj, ne_eq, Part.mem_some_iff, elim'_some]
             classical
-            refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ?_⟩
-            · replace h := Subtype.ext_iff.mp h
-              dsimp at h
-              rw [h]
-              rw [← Part.mem_toOption] at hw
-              exact Eq.symm ((fun {α} {a} {b} ↦ mem_def.mp) hw)
-            · exact ⟨b, Part.mem_toOption.mp h.symm, rfl⟩
+            refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩
+            rw [Subtype.ext_iff] at h
+            dsimp at h
+            rw [h]
+            rw [← Part.mem_toOption, mem_def] at hw
+            exact hw.symm
   counitIso :=
     NatIso.ofComponents
       (fun X ↦ Pointed.Iso.mk (by classical exact Equiv.optionSubtypeNe X.point) (by rfl))
diff --git a/Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean b/Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@@ -13,8 +13,8 @@ public import Mathlib.Tactic.CategoryTheory.Elementwise
 # Computation of `Over A` for a presheaf `A`
 
 Let `A : Cᵒᵖ ⥤ Type v` be a presheaf. In this file, we construct an equivalence
-`e : Over A ≌ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v` and show that there is a
-quasi-commutative diagram
+`e : Over A ≌ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v` and show that there is a quasi-commutative
+diagram
 
 ```
 CostructuredArrow yoneda A      ⥤      Over A
@@ -77,9 +77,7 @@ variable {C : Type u} [Category.{v} C] {A : Cᵒᵖ ⥤ Type v}
 
 namespace OverPresheafAux
 
-/-!
-### Construction of the forward functor `Over A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v`
--/
+/-! ### Construction of the forward functor `Over A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v` -/
 
 /-- Via the Yoneda lemma, `u : F.obj (op X)` defines a natural transformation `yoneda.obj X ⟶ F`
 and via the element `η.app (op X) u` also a morphism `yoneda.obj X ⟶ A`. This structure
@@ -384,9 +382,9 @@ end YonedaCollection
 
 /-- Given `F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v`, this is the presheaf that is given by
 `YonedaCollection F X` on objects. -/
-@[simps obj map]
-def yonedaCollectionPresheaf (A : Cᵒᵖ ⥤ Type v)
-    (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) : Cᵒᵖ ⥤ Type v where
+@[simps]
+def yonedaCollectionPresheaf (A : Cᵒᵖ ⥤ Type v) (F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) :
+    Cᵒᵖ ⥤ Type v where
   obj X := YonedaCollection F X.unop
   map f := TypeCat.ofHom (YonedaCollection.map₂ F f.unop)
 
@@ -401,7 +399,7 @@ def yonedaCollectionPresheafMap₁ {F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤
     simp
 
 /-- This is the functor `F ↦ X ↦ YonedaCollection F X`. -/
-@[simps obj map]
+@[simps]
 def yonedaCollectionFunctor (A : Cᵒᵖ ⥤ Type v) :
     ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) ⥤ Cᵒᵖ ⥤ Type v where
   obj := yonedaCollectionPresheaf A
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -214,6 +214,7 @@ variable {D : Type*} [Category* D] {FD : outParam <| D → D → Type*}
     {CD : outParam <| D → Type w}
     [outParam <| ∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD]
 
+-- TODO: generate this lemma with the `elementwise` attribute.
 @[simp]
 lemma NatTrans.naturality_apply {F G : C ⥤ D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y)
     (x : ToType (F.obj X)) :
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean b/Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean
@@ -38,6 +38,12 @@ namespace ConcreteCategory
 
 section
 
+instance [(forget C).PreservesMonomorphisms] {X Y : C} (f : X ⟶ Y) [Mono f] :
+    Mono (TypeCat.ofHom f) := Functor.map_mono (forget C) f
+
+instance [(forget C).PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y) [Epi f] :
+    Epi (TypeCat.ofHom f) := Functor.map_epi (forget C) f
+
 /-- In any concrete category, injective morphisms are monomorphisms. -/
 theorem mono_of_injective {X Y : C} (f : X ⟶ Y) (i : Function.Injective f) :
     Mono f :=
@@ -98,7 +104,7 @@ lemma surjective_eq_epimorphisms_iff :
     have : Epi f := hf
     change Function.Surjective ((forget C).map f)
     rw [← epi_iff_surjective]
-    exact Functor.map_epi _ f
+    infer_instance
 
 lemma injective_eq_monomorphisms_iff :
     MorphismProperty.injective C = monomorphisms C ↔ (forget C).PreservesMonomorphisms := by
@@ -115,7 +121,7 @@ lemma injective_eq_monomorphisms_iff :
     have : Mono f := hf
     change Function.Injective ((forget C).map f)
     rw [← mono_iff_injective]
-    exact Functor.map_mono _ f
+    infer_instance
 
 lemma injective_eq_monomorphisms [(forget C).PreservesMonomorphisms] :
     MorphismProperty.injective C = monomorphisms C := by
@@ -151,7 +157,7 @@ open CategoryTheory.Limits
 
 theorem injective_of_mono_of_preservesPullback {X Y : C} (f : X ⟶ Y) [Mono f]
     [PreservesLimitsOfShape WalkingCospan (forget C)] : Function.Injective f :=
-  (mono_iff_injective ((forget C).map f)).mp (Functor.map_mono _ f)
+  (mono_iff_injective ((forget C).map f)).mp inferInstance
 
 theorem mono_iff_injective_of_preservesPullback {X Y : C} (f : X ⟶ Y)
     [PreservesLimitsOfShape WalkingCospan (forget C)] : Mono f ↔ Function.Injective f :=
@@ -164,7 +170,7 @@ theorem epi_of_surjective {X Y : C} (f : X ⟶ Y) (s : Function.Surjective f) :
 
 theorem surjective_of_epi_of_preservesPushout {X Y : C} (f : X ⟶ Y) [Epi f]
     [PreservesColimitsOfShape WalkingSpan (forget C)] : Function.Surjective f :=
-  (epi_iff_surjective ((forget C).map f)).mp (Functor.map_epi _ f)
+  (epi_iff_surjective ((forget C).map f)).mp inferInstance
 
 theorem epi_iff_surjective_of_preservesPushout {X Y : C} (f : X ⟶ Y)
     [PreservesColimitsOfShape WalkingSpan (forget C)] : Epi f ↔ Function.Surjective f :=
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Forget.lean b/Mathlib/CategoryTheory/ConcreteCategory/Forget.lean
@@ -55,12 +55,14 @@ instance : (forget C).Faithful where
 
 variable {C}
 
--- TODO: rename
 @[simp]
-lemma ConcreteCategory.forget_map_eq_coe {X Y : C} (f : X ⟶ Y) :
+lemma ConcreteCategory.forget_map_eq_ofHom {X Y : C} (f : X ⟶ Y) :
     (forget C).map f = TypeCat.ofHom f :=
   rfl
 
+@[deprecated (since := "2026-04-11")] alias ConcreteCategory.forget_map_eq_coe :=
+  ConcreteCategory.forget_map_eq_ofHom
+
 theorem forget_obj (X : C) : (forget C).obj X = ToType X := rfl
 
 /-- Analogue of `congr_fun h x`,
diff --git a/Mathlib/CategoryTheory/Galois/Topology.lean b/Mathlib/CategoryTheory/Galois/Topology.lean
@@ -100,7 +100,7 @@ lemma autEmbedding_range :
 /-- The image of `Aut F` in `∀ X, Aut (F.obj X)` is closed. -/
 lemma autEmbedding_range_isClosed : IsClosed (Set.range (autEmbedding F)) := by
   rw [autEmbedding_range]
-  refine isClosed_iInter (fun f ↦ isClosed_eq (by fun_prop) (by fun_prop))
+  exact isClosed_iInter (fun f ↦ isClosed_eq (by fun_prop) (by fun_prop))
 
 lemma autEmbedding_isClosedEmbedding : IsClosedEmbedding (autEmbedding F) where
   eq_induced := rfl
diff --git a/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean b/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
@@ -88,6 +88,8 @@ theorem colimitLimitToLimitColimit_injective :
         (colimit.ι ((curry.obj F).obj j) ky)
           ((limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j) y) := by
       simpa using ConcreteCategory.congr_arg (limit.π (curry.obj F ⋙ colim) j) h
+    -- and they are equations in a filtered colimit,
+    -- so for each `j` we have some place `k j` to the right of both `kx` and `ky`
     simp only [colimit_eq_iff] at h
     let k j := (h j).choose
     let f : ∀ j, kx ⟶ k j := fun j => (h j).choose_spec.choose
diff --git a/Mathlib/CategoryTheory/Limits/FintypeCat.lean b/Mathlib/CategoryTheory/Limits/FintypeCat.lean
@@ -38,7 +38,7 @@ instance {J : Type} [SmallCategory J] (K : J ⥤ FintypeCat.{u}) (j : J) :
 /-- Any functor from a finite category to `Type*` that only involves finite objects,
 has a finite limit. -/
 noncomputable instance finiteLimitOfFiniteDiagram {J : Type} [SmallCategory J] [FinCategory J]
-    (K : J ⥤ Type u) [∀ j, Finite (K.obj j)] : Fintype (limit K) := by
+    (K : J ⥤ Type*) [∀ j, Finite (K.obj j)] : Fintype (limit K) := by
   have : Fintype (sections K) := Fintype.ofFinite (sections K)
   exact Fintype.ofEquiv (sections K) (Types.limitEquivSections K).symm
 
diff --git a/Mathlib/CategoryTheory/Limits/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Presheaf.lean
diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean b/Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean
diff --git a/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean b/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean
diff --git a/Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean b/Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean
diff --git a/Mathlib/Order/Category/PartOrd.lean b/Mathlib/Order/Category/PartOrd.lean
diff --git a/Mathlib/Order/Category/Preord.lean b/Mathlib/Order/Category/Preord.lean
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
