From b59de54138beca49cf0a0b1709023f716ef018c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dagur=20T=C3=B3mas=20=C3=81sgeirsson?=
 <100034030+mattrobball@users.noreply.github.com>
Date: Thu, 30 May 2024 08:29:57 +0000
Subject: [PATCH] chore(Category/TopCat): cleanup (#13170)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR removes an instance (`ConcreteCategory.instFunLike`) that was mistakenly made global during the port and starts the clean up. It significantly speeds up CI since simp is more efficient.

Unfortunately, some `simp`'s and `rw`'s needed to be changed to `erw` as a result.

Zulip discussion: [#mathlib4 > ConcreteCategory.instFunLike became a global instance](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ConcreteCategory.2EinstFunLike.20became.20a.20.20global.20instance)

Issue: #13342



Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: dagurtomas <dagurtomas@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: erdOne <the.erd.one@gmail.com>
Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
---
 Mathlib/AlgebraicGeometry/AffineScheme.lean   | 11 +--
 Mathlib/AlgebraicGeometry/Gluing.lean         | 13 ++--
 .../Morphisms/QuasiCompact.lean               |  2 +-
 Mathlib/AlgebraicGeometry/OpenImmersion.lean  | 27 ++++---
 Mathlib/AlgebraicGeometry/Restrict.lean       |  6 +-
 Mathlib/AlgebraicGeometry/Scheme.lean         |  1 +
 .../FundamentalGroupoid/Basic.lean            |  4 +-
 .../ConcreteCategory/Basic.lean               |  1 +
 Mathlib/Condensed/TopComparison.lean          |  3 +-
 .../LocallyRingedSpace/HasColimits.lean       |  2 +-
 .../Geometry/RingedSpace/OpenImmersion.lean   | 30 ++++++--
 .../RingedSpace/PresheafedSpace/Gluing.lean   | 21 ++---
 Mathlib/MeasureTheory/Category/MeasCat.lean   |  3 +
 Mathlib/Topology/Category/CompHaus/Basic.lean |  4 +
 .../Category/CompHaus/EffectiveEpi.lean       |  6 ++
 .../Topology/Category/CompHaus/Limits.lean    |  6 ++
 .../Category/LightProfinite/Basic.lean        |  3 +
 .../Category/LightProfinite/EffectiveEpi.lean |  6 ++
 .../Category/LightProfinite/IsLight.lean      |  3 +
 .../Category/LightProfinite/Limits.lean       |  6 ++
 .../Topology/Category/Profinite/Basic.lean    |  3 +
 .../Category/Profinite/CofilteredLimit.lean   |  3 +
 .../Category/Profinite/EffectiveEpi.lean      |  6 ++
 .../Topology/Category/Profinite/Limits.lean   |  6 ++
 .../Category/Profinite/Projective.lean        |  3 +
 Mathlib/Topology/Category/Stonean/Basic.lean  |  3 +
 Mathlib/Topology/Category/TopCat/Basic.lean   | 30 ++++++--
 .../Category/TopCat/Limits/Cofiltered.lean    |  2 +-
 .../Category/TopCat/Limits/Products.lean      | 42 +++++-----
 .../Category/TopCat/Limits/Pullbacks.lean     | 76 ++++++++++++-------
 Mathlib/Topology/Category/UniformSpace.lean   |  2 +
 Mathlib/Topology/Gluing.lean                  | 33 +++++---
 Mathlib/Topology/Order/Category/AlexDisc.lean |  3 +
 .../Order/Category/FrameAdjunction.lean       |  3 +
 .../Topology/Sheaves/LocallySurjective.lean   |  3 +
 Mathlib/Topology/Sheaves/Operations.lean      |  2 +-
 Mathlib/Topology/Sheaves/Stalks.lean          |  5 +-
 37 files changed, 263 insertions(+), 120 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
index b4e00c28cd3c2..e05618ae911c8 100644
--- a/Mathlib/AlgebraicGeometry/AffineScheme.lean
+++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -273,9 +273,9 @@ instance isOpenImmersion_fromSpec :
 theorem fromSpec_range :
     Set.range hU.fromSpec.1.base = (U : Set X) := by
   delta IsAffineOpen.fromSpec; dsimp
-  rw [← Category.assoc, coe_comp, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
+  rw [Function.comp.assoc, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
   · exact Subtype.range_coe
-  rw [← TopCat.epi_iff_surjective]
+  erw [← coe_comp, ← TopCat.epi_iff_surjective] -- now `erw` after #13170
   infer_instance
 #align algebraic_geometry.is_affine_open.from_Spec_range AlgebraicGeometry.IsAffineOpen.fromSpec_range
 
@@ -306,9 +306,9 @@ theorem _root_.AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion
   refine ⟨fun hU => @isAffineOfIso _ _
     (IsOpenImmersion.isoOfRangeEq (X.ofRestrict U.openEmbedding ≫ f) (Y.ofRestrict _) ?_).hom ?_ hU,
     fun hU => hU.imageIsOpenImmersion f⟩
-  · rw [Scheme.comp_val_base, coe_comp, Set.range_comp]
+  · erw [Scheme.comp_val_base, coe_comp, Set.range_comp] -- now `erw` after #13170
     dsimp [Opens.coe_inclusion, Scheme.restrict]
-    rw [Subtype.range_coe, Subtype.range_coe]
+    erw [Subtype.range_coe, Subtype.range_coe] -- now `erw` after #13170
     rfl
   · infer_instance
 #align algebraic_geometry.is_affine_open_iff_of_is_open_immersion AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion
@@ -515,11 +515,12 @@ theorem fromSpec_primeIdealOf (x : U) :
   -- Porting note: in the porting note of `Scheme.comp_val_base`, it says that `elementwise` is
   -- unnecessary, indeed, the linter did not like it, so I just use `elementwise_of%` instead of
   -- adding the corresponding lemma in `Scheme.lean` file
-  rw [← elementwise_of% Scheme.comp_val_base]
+  erw [← elementwise_of% Scheme.comp_val_base] -- now `erw` after #13170
   simp only [Scheme.Γ_obj, unop_op, Scheme.restrict_presheaf_obj, Category.assoc, ←
     Functor.map_comp_assoc, ← op_comp, ← Functor.map_comp, eqToHom_trans, eqToHom_refl, op_id,
     CategoryTheory.Functor.map_id, Category.id_comp, Iso.hom_inv_id_assoc,
     Scheme.ofRestrict_val_base, Scheme.restrict_carrier, Opens.coe_inclusion]
+  rfl -- `rfl` was not needed before #13170
 #align algebraic_geometry.is_affine_open.from_Spec_prime_ideal_of AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf
 
 set_option backward.isDefEq.lazyWhnfCore false in -- See https://github.com/leanprover-community/mathlib4/issues/12534
diff --git a/Mathlib/AlgebraicGeometry/Gluing.lean b/Mathlib/AlgebraicGeometry/Gluing.lean
index ae5d5280a4b4c..201095e4195f7 100644
--- a/Mathlib/AlgebraicGeometry/Gluing.lean
+++ b/Mathlib/AlgebraicGeometry/Gluing.lean
@@ -132,9 +132,7 @@ def gluedScheme : Scheme := by
   swap
   · exact (D.U i).affineCover.map y
   constructor
-  · -- Without removing `Spec.topObj_forget`, we need an `erw` in the following line.
-    dsimp [-Spec.topObj_forget]
-    rw [coe_comp, Set.range_comp]
+  · erw [TopCat.coe_comp, Set.range_comp] -- now `erw` after #13170
     refine' Set.mem_image_of_mem _ _
     exact (D.U i).affineCover.Covers y
   · infer_instance
@@ -249,7 +247,9 @@ theorem ι_eq_iff (i j : D.J) (x : (D.U i).carrier) (y : (D.U j).carrier) :
       D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
       i j x y)
   rw [← ((TopCat.mono_iff_injective D.isoCarrier.inv).mp _).eq_iff]
-  · simp_rw [← comp_apply, ← D.ι_isoCarrier_inv]; rfl
+  · erw [← comp_apply] -- now `erw` after #13170
+    simp_rw [← D.ι_isoCarrier_inv]
+    rfl -- `rfl` was not needed before #13170
   · infer_instance
 #align algebraic_geometry.Scheme.glue_data.ι_eq_iff AlgebraicGeometry.Scheme.GlueData.ι_eq_iff
 
@@ -372,7 +372,8 @@ theorem fromGlued_injective : Function.Injective 𝒰.fromGlued.1.base := by
   intro x y h
   obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
   obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y
-  simp_rw [← comp_apply, ← SheafedSpace.comp_base, ← LocallyRingedSpace.comp_val] at h
+  erw [← comp_apply, ← comp_apply] at h -- now `erw` after #13170
+  simp_rw [← SheafedSpace.comp_base, ← LocallyRingedSpace.comp_val] at h
   erw [ι_fromGlued, ι_fromGlued] at h
   let e :=
     (TopCat.pullbackConeIsLimit _ _).conePointUniqueUpToIso
@@ -427,7 +428,7 @@ instance : Epi 𝒰.fromGlued.val.base := by
   intro x
   obtain ⟨y, h⟩ := 𝒰.Covers x
   use (𝒰.gluedCover.ι (𝒰.f x)).1.base y
-  rw [← comp_apply]
+  erw [← comp_apply] -- now `erw` after #13170
   rw [← 𝒰.ι_fromGlued (𝒰.f x)] at h
   exact h
 
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
index e7292244469dc..f81b372b188ab 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
@@ -68,7 +68,7 @@ instance quasiCompactComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiCom
     [QuasiCompact g] : QuasiCompact (f ≫ g) := by
   constructor
   intro U hU hU'
-  rw [Scheme.comp_val_base, coe_comp, Set.preimage_comp]
+  rw [Scheme.comp_val_base, TopCat.coe_comp, Set.preimage_comp]
   apply QuasiCompact.isCompact_preimage
   · exact Continuous.isOpen_preimage (by
     -- Porting note: `continuity` failed
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
index 205f988f6fbd3..310d67981e56f 100644
--- a/Mathlib/AlgebraicGeometry/OpenImmersion.lean
+++ b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -119,11 +119,11 @@ def affineCover (X : Scheme.{u}) : OpenCover X where
     apply PresheafedSpace.IsOpenImmersion.ofRestrict
   Covers := by
     intro x
-    erw [coe_comp]
+    erw [TopCat.coe_comp] -- now `erw` after #13170
     rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
     · erw [Subtype.range_coe_subtype]
       exact (X.local_affine x).choose.2
-    rw [← TopCat.epi_iff_surjective]
+    erw [← TopCat.epi_iff_surjective] -- now `erw` after #13170
     change Epi ((SheafedSpace.forget _).map (LocallyRingedSpace.forgetToSheafedSpace.map _))
     infer_instance
 #align algebraic_geometry.Scheme.affine_cover AlgebraicGeometry.Scheme.affineCover
@@ -146,7 +146,7 @@ def OpenCover.bind (f : ∀ x : 𝒰.J, OpenCover (𝒰.obj x)) : OpenCover X wh
     change x ∈ Set.range ((f (𝒰.f x)).map ((f (𝒰.f x)).f y) ≫ 𝒰.map (𝒰.f x)).1.base
     use z
     erw [comp_apply]
-    rw [hz, hy]
+    erw [hz, hy] -- now `erw` after #13170
   -- Porting note: weirdly, even though no input is needed, `inferInstance` does not work
   -- `PresheafedSpace.IsOpenImmersion.comp` is marked as `instance`
   IsOpen x := PresheafedSpace.IsOpenImmersion.comp _ _
@@ -175,10 +175,10 @@ def OpenCover.copy {X : Scheme.{u}} (𝒰 : OpenCover X) (J : Type*) (obj : J 
   { J, obj, map
     f := fun x => e₁.symm (𝒰.f x)
     Covers := fun x => by
-      rw [e₂, Scheme.comp_val_base, coe_comp, Set.range_comp, Set.range_iff_surjective.mpr,
+      rw [e₂, Scheme.comp_val_base, TopCat.coe_comp, Set.range_comp, Set.range_iff_surjective.mpr,
         Set.image_univ, e₁.rightInverse_symm]
       · exact 𝒰.Covers x
-      · rw [← TopCat.epi_iff_surjective]; infer_instance
+      · erw [← TopCat.epi_iff_surjective]; infer_instance -- now `erw` after #13170
     -- Porting note: weirdly, even though no input is needed, `inferInstance` does not work
     -- `PresheafedSpace.IsOpenImmersion.comp` is marked as `instance`
     IsOpen := fun i => by rw [e₂]; exact PresheafedSpace.IsOpenImmersion.comp _ _ }
@@ -567,7 +567,7 @@ theorem range_pullback_snd_of_left :
   · erw [TopCat.pullback_snd_image_fst_preimage]
     rw [Set.image_univ]
     rfl
-  rw [← TopCat.epi_iff_surjective]
+  erw [← TopCat.epi_iff_surjective] -- now `erw` after #13170
   infer_instance
 #align algebraic_geometry.IsOpenImmersion.range_pullback_snd_of_left AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left
 
@@ -584,14 +584,14 @@ theorem range_pullback_fst_of_right :
   · erw [TopCat.pullback_fst_image_snd_preimage]
     rw [Set.image_univ]
     rfl
-  rw [← TopCat.epi_iff_surjective]
+  erw [← TopCat.epi_iff_surjective] -- now `erw` after #13170
   infer_instance
 #align algebraic_geometry.IsOpenImmersion.range_pullback_fst_of_right AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right
 
 theorem range_pullback_to_base_of_left :
     Set.range (pullback.fst ≫ f : pullback f g ⟶ Z).1.base =
       Set.range f.1.base ∩ Set.range g.1.base := by
-  rw [pullback.condition, Scheme.comp_val_base, coe_comp, Set.range_comp,
+  rw [pullback.condition, Scheme.comp_val_base, TopCat.coe_comp, Set.range_comp,
     range_pullback_snd_of_left, Opens.carrier_eq_coe,
     Opens.map_obj, Opens.coe_mk, Set.image_preimage_eq_inter_range]
 #align algebraic_geometry.IsOpenImmersion.range_pullback_to_base_of_left AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left
@@ -599,8 +599,9 @@ theorem range_pullback_to_base_of_left :
 theorem range_pullback_to_base_of_right :
     Set.range (pullback.fst ≫ g : pullback g f ⟶ Z).1.base =
       Set.range g.1.base ∩ Set.range f.1.base := by
-  rw [Scheme.comp_val_base, coe_comp, Set.range_comp, range_pullback_fst_of_right, Opens.map_obj,
-    Opens.carrier_eq_coe, Opens.coe_mk, Set.image_preimage_eq_inter_range, Set.inter_comm]
+  rw [Scheme.comp_val_base, TopCat.coe_comp, Set.range_comp, range_pullback_fst_of_right,
+    Opens.map_obj, Opens.carrier_eq_coe, Opens.coe_mk, Set.image_preimage_eq_inter_range,
+    Set.inter_comm]
 #align algebraic_geometry.IsOpenImmersion.range_pullback_to_base_of_right AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_right
 
 /-- The universal property of open immersions:
@@ -740,8 +741,7 @@ def Scheme.OpenCover.pullbackCover {X W : Scheme.{u}} (𝒰 : X.OpenCover) (f :
       show _ = (pullback.fst : pullback f (𝒰.map (𝒰.f (f.1.base x))) ⟶ _).1.base from
         PreservesPullback.iso_hom_fst Scheme.forgetToTop f (𝒰.map (𝒰.f (f.1.base x)))]
     -- Porting note: `rw` to `erw` on this single lemma
-    erw [coe_comp]
-    rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ,
+    rw [TopCat.coe_comp, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ,
       TopCat.pullback_fst_range]
     · obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x)
       exact ⟨y, h.symm⟩
@@ -763,8 +763,7 @@ def Scheme.OpenCover.pullbackCover' {X W : Scheme.{u}} (𝒰 : X.OpenCover) (f :
       show _ = (pullback.snd : pullback (𝒰.map (𝒰.f (f.1.base x))) f ⟶ _).1.base from
         PreservesPullback.iso_hom_snd Scheme.forgetToTop (𝒰.map (𝒰.f (f.1.base x))) f]
     -- Porting note: `rw` to `erw` on this single lemma
-    erw [coe_comp]
-    rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ,
+    rw [TopCat.coe_comp, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ,
       TopCat.pullback_snd_range]
     · obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x)
       exact ⟨y, h⟩
diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean
index 001f9b9febb82..10ae4065aa740 100644
--- a/Mathlib/AlgebraicGeometry/Restrict.lean
+++ b/Mathlib/AlgebraicGeometry/Restrict.lean
@@ -182,7 +182,7 @@ def Scheme.restrictRestrictComm (X : Scheme.{u}) (U V : Opens X.carrier) :
     X ∣_ᵤ U ∣_ᵤ ιOpens U ⁻¹ᵁ V ≅ X ∣_ᵤ V ∣_ᵤ ιOpens V ⁻¹ᵁ U := by
   refine IsOpenImmersion.isoOfRangeEq (ιOpens _ ≫ ιOpens U) (ιOpens _ ≫ ιOpens V) ?_
   simp only [Scheme.restrict_carrier, Scheme.ofRestrict_val_base, Scheme.comp_coeBase,
-    CategoryTheory.coe_comp, Opens.coe_inclusion, Set.range_comp, Opens.map]
+    TopCat.coe_comp, Opens.coe_inclusion, Set.range_comp, Opens.map]
   rw [Subtype.range_val, Subtype.range_val]
   dsimp
   rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range,
@@ -194,7 +194,7 @@ def Scheme.restrictRestrict (X : Scheme.{u}) (U : Opens X.carrier) (V : Opens (X
     X ∣_ᵤ U ∣_ᵤ V ≅ X ∣_ᵤ U.openEmbedding.isOpenMap.functor.obj V := by
   refine IsOpenImmersion.isoOfRangeEq (ιOpens _ ≫ ιOpens U) (ιOpens _) ?_
   simp only [Scheme.restrict_carrier, Scheme.ofRestrict_val_base, Scheme.comp_coeBase,
-    CategoryTheory.coe_comp, Opens.coe_inclusion, Set.range_comp, Opens.map]
+    TopCat.coe_comp, Opens.coe_inclusion, Set.range_comp, Opens.map]
   rw [Subtype.range_val, Subtype.range_val]
   rfl
 
@@ -225,7 +225,7 @@ noncomputable abbrev Scheme.restrictMapIso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsI
     (H := PresheafedSpace.IsOpenImmersion.comp (hf := inferInstance) (hg := inferInstance))
     (Y.ofRestrict _) _
   dsimp [restrict]
-  rw [coe_comp, Set.range_comp, Opens.coe_inclusion, Subtype.range_val, Subtype.range_coe]
+  rw [Set.range_comp, Subtype.range_val, Subtype.range_coe]
   refine' @Set.image_preimage_eq _ _ f.1.base U.1 _
   rw [← TopCat.epi_iff_surjective]
   infer_instance
diff --git a/Mathlib/AlgebraicGeometry/Scheme.lean b/Mathlib/AlgebraicGeometry/Scheme.lean
index b5d56757ba737..68aab9a0ab2a6 100644
--- a/Mathlib/AlgebraicGeometry/Scheme.lean
+++ b/Mathlib/AlgebraicGeometry/Scheme.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import Mathlib.AlgebraicGeometry.Spec
 import Mathlib.Algebra.Category.Ring.Constructions
+import Mathlib.CategoryTheory.Elementwise
 
 #align_import algebraic_geometry.Scheme from "leanprover-community/mathlib"@"88474d1b5af6d37c2ab728b757771bced7f5194c"
 
diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
index 124a010bc1da5..f391ce72875f4 100644
--- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
+++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
@@ -369,9 +369,7 @@ def fundamentalGroupoidFunctor : TopCat ⥤ CategoryTheory.Grpd where
       map_id := fun X => rfl
       map_comp := fun {x y z} p q => by
         refine Quotient.inductionOn₂ p q fun a b => ?_
-        simp only [comp_eq, ← Path.Homotopic.map_lift, ← Path.Homotopic.comp_lift, Path.map_trans]
-        -- This was not needed before leanprover/lean4#2644
-        erw [ ← Path.Homotopic.comp_lift]; rfl}
+        simp only [comp_eq, ← Path.Homotopic.map_lift, ← Path.Homotopic.comp_lift, Path.map_trans] }
   map_id X := by
     simp only
     change _ = (⟨_, _, _⟩ : FundamentalGroupoid X ⥤ FundamentalGroupoid X)
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
index 610571ce87a12..51a98723e4751 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -95,6 +95,7 @@ variable {C : Type u} [Category.{v} C] [ConcreteCategory.{w} C]
 -- Porting note: forget_obj_eq_coe has become a syntactic tautology.
 #noalign category_theory.forget_obj_eq_coe
 
+/-- In any concrete category, `(forget C).map` is injective. -/
 abbrev ConcreteCategory.instFunLike {X Y : C} : FunLike (X ⟶ Y) X Y where
   coe f := (forget C).map f
   coe_injective' _ _ h := (forget C).map_injective h
diff --git a/Mathlib/Condensed/TopComparison.lean b/Mathlib/Condensed/TopComparison.lean
index db2547006cdf8..c54b63a6e104f 100644
--- a/Mathlib/Condensed/TopComparison.lean
+++ b/Mathlib/Condensed/TopComparison.lean
@@ -53,7 +53,8 @@ theorem factorsThrough_of_pullbackCondition {Z B : C} {π : Z ⟶ B} [HasPullbac
   have h₂ : ∀ y, G.map pullback.snd ((PreservesPullback.iso G π π).inv y) =
       pullback.snd (f := G.map π) (g := G.map π) y := by
     simp only [← PreservesPullback.iso_inv_snd]; intro y; rfl
-  erw [h₁, h₂] at ha'
+  erw [h₁, h₂, TopCat.pullbackIsoProdSubtype_inv_fst_apply,
+    TopCat.pullbackIsoProdSubtype_inv_snd_apply] at ha'
   simpa using ha'
 
 /--
diff --git a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
index 57c128acf67ca..8adbdf2c6d653 100644
--- a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
+++ b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
@@ -215,7 +215,7 @@ theorem imageBasicOpen_image_open :
     IsOpen ((coequalizer.π f.1 g.1).base '' (imageBasicOpen f g U s).1) := by
   rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.1
     g.1)).isOpen_preimage, TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]
-  erw [← coe_comp]
+  erw [← TopCat.coe_comp]
   rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]
   dsimp only [SheafedSpace.forget]
   -- Porting note (#11224): change `rw` to `erw`
diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
index 410124117c27c..bf6a069194833 100644
--- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
+++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
@@ -165,8 +165,8 @@ instance comp {Z : PresheafedSpace C} (f : X ⟶ Y) [hf : IsOpenImmersion f] (g
         ext1
         dsimp only [IsOpenMap.functor_obj_coe]
         -- Porting note: slightly more hand holding here: `g ∘ f` and `fun x => g (f x)`
-        rw [comp_base, coe_comp, show g.base ∘ f.base = fun x => g.base (f.base x) from rfl,
-          ← Set.image_image]
+        erw [comp_base, coe_comp, show g.base ∘ f.base = fun x => g.base (f.base x) from rfl,
+          ← Set.image_image]  -- now `erw` after #13170
       rw [this]
       infer_instance
     have : IsIso (f.c.app (op <| (Opens.map g.base).obj ((IsOpenMap.functor h).obj U))) := by
@@ -174,8 +174,9 @@ instance comp {Z : PresheafedSpace C} (f : X ⟶ Y) [hf : IsOpenImmersion f] (g
         ext1
         dsimp only [Opens.map_coe, IsOpenMap.functor_obj_coe, comp_base]
         -- Porting note: slightly more hand holding here: `g ∘ f` and `fun x => g (f x)`
-        rw [coe_comp, show g.base ∘ f.base = fun x => g.base (f.base x) from rfl,
+        erw [coe_comp, show g.base ∘ f.base = fun x => g.base (f.base x) from rfl,
           ← Set.image_image g.base f.base, Set.preimage_image_eq _ hg.base_open.inj]
+           -- now `erw` after #13170
       rw [this]
       infer_instance
     apply IsIso.comp_isIso
@@ -364,10 +365,22 @@ def pullbackConeOfLeftFst :
                   · rintro _ ⟨_, h₁, h₂⟩
                     use (TopCat.pullbackIsoProdSubtype _ _).inv ⟨⟨_, _⟩, h₂⟩
                     -- Porting note: need a slight hand holding
+                    -- used to be `simpa using h₁` before #13170
                     change _ ∈ _ ⁻¹' _ ∧ _
-                    simpa using h₁
+                    simp only [TopCat.coe_of, restrict_carrier, Set.preimage_id', Set.mem_preimage,
+                      SetLike.mem_coe]
+                    constructor
+                    · change _ ∈ U.unop at h₁
+                      convert h₁
+                      erw [TopCat.pullbackIsoProdSubtype_inv_fst_apply]
+                    · erw [TopCat.pullbackIsoProdSubtype_inv_snd_apply]
                   · rintro _ ⟨x, h₁, rfl⟩
-                    exact ⟨_, h₁, ConcreteCategory.congr_hom pullback.condition x⟩))
+                    -- next line used to be
+                    --  `exact ⟨_, h₁, ConcreteCategory.congr_hom pullback.condition x⟩))`
+                    -- before #13170
+                    refine ⟨_, h₁, ?_⟩
+                    change (_ ≫ f.base) _ = (_ ≫ g.base) _
+                    rw [pullback.condition]))
       naturality := by
         intro U V i
         induction U using Opposite.rec'
@@ -432,7 +445,7 @@ def pullbackConeOfLeftLift : s.pt ⟶ (pullbackConeOfLeft f g).pt where
                   erw [← this]
                   dsimp [s']
                   -- Porting note: need a bit more hand holding here about function composition
-                  rw [coe_comp, show ∀ f g, f ∘ g = fun x => f (g x) from fun _ _ => rfl]
+                  rw [show ∀ f g, f ∘ g = fun x => f (g x) from fun _ _ => rfl]
                   erw [← Set.preimage_preimage]
                 erw [Set.preimage_image_eq _
                     (TopCat.snd_openEmbedding_of_left_openEmbedding hf.base_open g.base).inj]
@@ -1169,7 +1182,8 @@ theorem lift_range (H' : Set.range g.1.base ⊆ Set.range f.1.base) :
   have : _ = (pullback.fst : pullback f g ⟶ _).val.base :=
     PreservesPullback.iso_hom_fst
       (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) f g
-  rw [LocallyRingedSpace.comp_val, SheafedSpace.comp_base, ← this, ← Category.assoc, coe_comp]
+  erw [LocallyRingedSpace.comp_val, SheafedSpace.comp_base, ← this, ← Category.assoc, coe_comp]
+   -- now `erw` after #13170
   rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
   -- Porting note (#11224): change `rw` to `erw` on this lemma
   · erw [TopCat.pullback_fst_range]
@@ -1177,7 +1191,7 @@ theorem lift_range (H' : Set.range g.1.base ⊆ Set.range f.1.base) :
     constructor
     · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
     · rintro ⟨y, eq⟩; exact ⟨y, eq.symm⟩
-  · rw [← TopCat.epi_iff_surjective]
+  · erw [← TopCat.epi_iff_surjective] -- now `erw` after #13170
     rw [show (inv (pullback.snd : pullback f g ⟶ _)).val.base = _ from
         (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _).map_inv _]
     infer_instance
diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
index 68cee56441288..9c6e083518411 100644
--- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
+++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -144,9 +144,10 @@ theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) :
   rw [Set.image_comp]
   -- Porting note: `rw` to `erw` on `coe_comp`
   erw [coe_comp]
-  rw [Set.preimage_comp, Set.image_preimage_eq, TopCat.pullback_snd_image_fst_preimage]
+  erw [Set.preimage_comp, Set.image_preimage_eq, TopCat.pullback_snd_image_fst_preimage]
+   -- now `erw` after #13170
   · rfl
-  rw [← TopCat.epi_iff_surjective]
+  erw [← TopCat.epi_iff_surjective] -- now `erw` after #13170
   infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.pullback_base AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base
 
@@ -202,14 +203,14 @@ theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)
     erw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]
     swap
     · refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
-      rw [← comp_apply, ← comp_base, D.t_inv, id_base, id_apply]
+      erw [← comp_apply, ← comp_base, D.t_inv, id_base, id_apply] -- now `erw` after #13170
     refine congr_arg (_ '' ·) ?_
     refine congr_fun ?_ _
     refine Set.image_eq_preimage_of_inverse ?_ ?_
     · intro x
-      rw [← comp_apply, ← comp_base, IsIso.inv_hom_id, id_base, id_apply]
+      erw [← comp_apply, ← comp_base, IsIso.inv_hom_id, id_base, id_apply] -- now `erw` after #13170
     · intro x
-      rw [← comp_apply, ← comp_base, IsIso.hom_inv_id, id_base, id_apply]
+      erw [← comp_apply, ← comp_base, IsIso.hom_inv_id, id_base, id_apply] -- now `erw` after #13170
   · rw [← IsIso.eq_inv_comp, IsOpenImmersion.inv_invApp, Category.assoc,
       (D.t' k i j).c.naturality_assoc]
     simp_rw [← Category.assoc]
@@ -261,15 +262,15 @@ theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
   erw [Set.preimage_image_eq]
   · refine Eq.trans (D.toTopGlueData.preimage_image_eq_image' _ _ _) ?_
     dsimp
-    rw [coe_comp, Set.image_comp]
+    rw [Set.image_comp]
     refine congr_arg (_ '' ·) ?_
     rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]
     swap
-    · apply CategoryTheory.ConcreteCategory.bijective_of_isIso
+    · exact CategoryTheory.ConcreteCategory.bijective_of_isIso (C := TopCat) _
     change (D.t i j ≫ D.t j i).base '' _ = _
     rw [𝖣.t_inv]
     simp
-  · rw [← coe_comp, ← TopCat.mono_iff_injective]
+  · erw [← coe_comp, ← TopCat.mono_iff_injective] -- now `erw` after #13170
     infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_image_preimage_eq AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq
 
@@ -428,9 +429,9 @@ theorem ιInvApp_π {i : D.J} (U : Opens (D.U i).carrier) :
     · exact h2.symm
     · have := D.ι_gluedIso_inv (PresheafedSpace.forget _) i
       dsimp at this
-      rw [← this, coe_comp]
+      erw [← this, coe_comp] -- now `erw` after #13170
       refine Function.Injective.comp ?_ (TopCat.GlueData.ι_injective D.toTopGlueData i)
-      rw [← TopCat.mono_iff_injective]
+      erw [← TopCat.mono_iff_injective] -- now `erw` after #13170
       infer_instance
   delta ιInvApp
   rw [limit.lift_π]
diff --git a/Mathlib/MeasureTheory/Category/MeasCat.lean b/Mathlib/MeasureTheory/Category/MeasCat.lean
index 524f1635491cc..8a53908624045 100644
--- a/Mathlib/MeasureTheory/Category/MeasCat.lean
+++ b/Mathlib/MeasureTheory/Category/MeasCat.lean
@@ -77,6 +77,9 @@ instance : ConcreteCategory MeasCat := by
 instance : Inhabited MeasCat :=
   ⟨MeasCat.of Empty⟩
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] ConcreteCategory.instFunLike
+
 /-- `Measure X` is the measurable space of measures over the measurable space `X`. It is the
 weakest measurable space, s.t. `fun μ ↦ μ s` is measurable for all measurable sets `s` in `X`. An
 important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad,
diff --git a/Mathlib/Topology/Category/CompHaus/Basic.lean b/Mathlib/Topology/Category/CompHaus/Basic.lean
index 0fb87df714b7f..80d90926faf63 100644
--- a/Mathlib/Topology/Category/CompHaus/Basic.lean
+++ b/Mathlib/Topology/Category/CompHaus/Basic.lean
@@ -9,6 +9,7 @@ import Mathlib.CategoryTheory.Monad.Limits
 import Mathlib.Topology.UrysohnsLemma
 import Mathlib.Topology.Category.TopCat.Limits.Basic
 import Mathlib.Data.Set.Subsingleton
+import Mathlib.CategoryTheory.Elementwise
 
 #align_import topology.category.CompHaus.basic from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
 
@@ -32,6 +33,9 @@ introduced.
 
 universe v u
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 open CategoryTheory
 
 /-- The type of Compact Hausdorff topological spaces. -/
diff --git a/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean b/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean
index 4e2ca46308a08..316a4f366fe1e 100644
--- a/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean
+++ b/Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean
@@ -35,6 +35,12 @@ As a consequence, we obtain instances that `CompHaus` is precoherent and preregu
 
 universe u
 
+/-
+Previously, this had accidentally been made a global instance,
+and we now turn it on locally when convenient.
+-/
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 open CategoryTheory Limits
 
 namespace CompHaus
diff --git a/Mathlib/Topology/Category/CompHaus/Limits.lean b/Mathlib/Topology/Category/CompHaus/Limits.lean
index b7809f86de225..ba1386c8a62d9 100644
--- a/Mathlib/Topology/Category/CompHaus/Limits.lean
+++ b/Mathlib/Topology/Category/CompHaus/Limits.lean
@@ -24,6 +24,12 @@ So far, we have the following:
 
 namespace CompHaus
 
+/-
+Previously, this had accidentally been made a global instance,
+and we now turn it on locally when convenient.
+-/
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 universe u w
 
 open CategoryTheory Limits
diff --git a/Mathlib/Topology/Category/LightProfinite/Basic.lean b/Mathlib/Topology/Category/LightProfinite/Basic.lean
index 58b410ae870be..2dcf511732918 100644
--- a/Mathlib/Topology/Category/LightProfinite/Basic.lean
+++ b/Mathlib/Topology/Category/LightProfinite/Basic.lean
@@ -26,6 +26,9 @@ universe u
 
 open CategoryTheory Limits Opposite FintypeCat
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] ConcreteCategory.instFunLike
+
 /-- A light profinite set is one which can be written as a sequential limit of finite sets. -/
 structure LightProfinite : Type (u+1) where
   /-- The indexing diagram. -/
diff --git a/Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean b/Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean
index 34983b2ab91ea..2c1c21c596a5d 100644
--- a/Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean
+++ b/Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean
@@ -18,6 +18,12 @@ that it is `Precoherent`.
 
 universe u
 
+/-
+Previously, this had accidentally been made a global instance,
+and we now turn it on locally when convenient.
+-/
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 open CategoryTheory Limits
 
 namespace LightProfinite
diff --git a/Mathlib/Topology/Category/LightProfinite/IsLight.lean b/Mathlib/Topology/Category/LightProfinite/IsLight.lean
index 471755a97cf5a..47dfffd6e46a5 100644
--- a/Mathlib/Topology/Category/LightProfinite/IsLight.lean
+++ b/Mathlib/Topology/Category/LightProfinite/IsLight.lean
@@ -34,6 +34,9 @@ universe u
 
 open CategoryTheory Limits FintypeCat Opposite TopologicalSpace
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] ConcreteCategory.instFunLike
+
 open scoped Classical
 
 namespace Profinite
diff --git a/Mathlib/Topology/Category/LightProfinite/Limits.lean b/Mathlib/Topology/Category/LightProfinite/Limits.lean
index a3fa134a70f77..298e66302597e 100644
--- a/Mathlib/Topology/Category/LightProfinite/Limits.lean
+++ b/Mathlib/Topology/Category/LightProfinite/Limits.lean
@@ -23,6 +23,12 @@ which may be useful due to their definitional properties.
 
 universe u w
 
+/-
+Previously, this had accidentally been made a global instance,
+and we now turn it on locally when convenient.
+-/
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 open CategoryTheory Profinite TopologicalSpace Limits
 
 namespace LightProfinite
diff --git a/Mathlib/Topology/Category/Profinite/Basic.lean b/Mathlib/Topology/Category/Profinite/Basic.lean
index 6d65b0322e81c..132f68a2fcc5a 100644
--- a/Mathlib/Topology/Category/Profinite/Basic.lean
+++ b/Mathlib/Topology/Category/Profinite/Basic.lean
@@ -35,6 +35,9 @@ profinite
 
 -/
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 set_option linter.uppercaseLean3 false
 
 universe v u
diff --git a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
index fac22f584ddd9..174fc335b55f7 100644
--- a/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
+++ b/Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
@@ -32,6 +32,9 @@ open CategoryTheory
 
 open CategoryTheory.Limits
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] ConcreteCategory.instFunLike
+
 universe u v
 
 variable {J : Type v} [SmallCategory J] [IsCofiltered J] {F : J ⥤ Profinite.{max u v}} (C : Cone F)
diff --git a/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean b/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean
index 54f2197a78166..a54841a79295b 100644
--- a/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean
+++ b/Mathlib/Topology/Category/Profinite/EffectiveEpi.lean
@@ -33,6 +33,12 @@ As a consequence, we obtain instances that `Profinite` is precoherent and prereg
 
 universe u
 
+/-
+Previously, this had accidentally been made a global instance,
+and we now turn it on locally when convenient.
+-/
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 open CategoryTheory Limits
 
 namespace Profinite
diff --git a/Mathlib/Topology/Category/Profinite/Limits.lean b/Mathlib/Topology/Category/Profinite/Limits.lean
index 8fefb8fd7b56e..6c227a2864bd7 100644
--- a/Mathlib/Topology/Category/Profinite/Limits.lean
+++ b/Mathlib/Topology/Category/Profinite/Limits.lean
@@ -25,6 +25,12 @@ namespace Profinite
 
 universe u w
 
+/-
+Previously, this had accidentally been made a global instance,
+and we now turn it on locally when convenient.
+-/
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 open CategoryTheory Limits
 
 section Pullbacks
diff --git a/Mathlib/Topology/Category/Profinite/Projective.lean b/Mathlib/Topology/Category/Profinite/Projective.lean
index 3cc8f29fec6a9..9b8986a6f6be7 100644
--- a/Mathlib/Topology/Category/Profinite/Projective.lean
+++ b/Mathlib/Topology/Category/Profinite/Projective.lean
@@ -31,6 +31,9 @@ universe u v w
 
 open CategoryTheory Function
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] ConcreteCategory.instFunLike
+
 namespace Profinite
 
 set_option linter.uppercaseLean3 false
diff --git a/Mathlib/Topology/Category/Stonean/Basic.lean b/Mathlib/Topology/Category/Stonean/Basic.lean
index 09b250fb7b8fc..d627205f3e506 100644
--- a/Mathlib/Topology/Category/Stonean/Basic.lean
+++ b/Mathlib/Topology/Category/Stonean/Basic.lean
@@ -37,6 +37,9 @@ universe u
 open CategoryTheory
 open scoped Topology
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] ConcreteCategory.instFunLike
+
 /-- `Stonean` is the category of extremally disconnected compact Hausdorff spaces. -/
 structure Stonean where
   /-- The underlying compact Hausdorff space of a Stonean space. -/
diff --git a/Mathlib/Topology/Category/TopCat/Basic.lean b/Mathlib/Topology/Category/TopCat/Basic.lean
index e4ba3bd9ae075..cc243d0b27f41 100644
--- a/Mathlib/Topology/Category/TopCat/Basic.lean
+++ b/Mathlib/Topology/Category/TopCat/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Scott Morrison, Mario Carneiro
 -/
 import Mathlib.CategoryTheory.ConcreteCategory.BundledHom
-import Mathlib.CategoryTheory.Elementwise
 import Mathlib.Topology.ContinuousFunction.Basic
 
 #align_import topology.category.Top.basic from "leanprover-community/mathlib"@"bcfa726826abd57587355b4b5b7e78ad6527b7e4"
@@ -56,11 +55,17 @@ instance topologicalSpaceUnbundled (X : TopCat) : TopologicalSpace X :=
 set_option linter.uppercaseLean3 false in
 #align Top.topological_space_unbundled TopCat.topologicalSpaceUnbundled
 
--- TODO(#13170): remove this global instance
--- Porting note: cannot find a coercion to function otherwise
-attribute [instance] ConcreteCategory.instFunLike
-instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where
-  coe f := f
+-- We leave this temporarily as a reminder of the downstream instances #13170
+-- -- Porting note: cannot find a coercion to function otherwise
+-- -- attribute [instance] ConcreteCategory.instFunLike in
+-- instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where
+--   coe (f : C(X, Y)) := f
+
+instance instFunLike (X Y : TopCat) : FunLike (X ⟶ Y) X Y :=
+  inferInstanceAs <| FunLike C(X, Y) X Y
+
+instance instMonoidHomClass (X Y : TopCat) : ContinuousMapClass (X ⟶ Y) X Y :=
+  inferInstanceAs <| ContinuousMapClass C(X, Y) X Y
 
 -- Porting note (#10618): simp can prove this; removed simp
 theorem id_app (X : TopCat.{u}) (x : ↑X) : (𝟙 X : X ⟶ X) x = x := rfl
@@ -73,6 +78,19 @@ theorem comp_app {X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
 set_option linter.uppercaseLean3 false in
 #align Top.comp_app TopCat.comp_app
 
+@[simp] theorem coe_id (X : TopCat.{u}) : (𝟙 X : X → X) = id := rfl
+
+@[simp] theorem coe_comp {X Y Z : TopCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g : X → Z) = g ∘ f := rfl
+
+@[simp]
+lemma hom_inv_id_apply {X Y : TopCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x :=
+  DFunLike.congr_fun f.hom_inv_id x
+
+@[simp]
+lemma inv_hom_id_apply {X Y : TopCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y :=
+  DFunLike.congr_fun f.inv_hom_id y
+
 /-- Construct a bundled `Top` from the underlying type and the typeclass. -/
 def of (X : Type u) [TopologicalSpace X] : TopCat :=
   -- Porting note: needed to call inferInstance
diff --git a/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean b/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean
index 2eebf60711290..fb7f0021e6a20 100644
--- a/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean
+++ b/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean
@@ -118,7 +118,7 @@ theorem isTopologicalBasis_cofiltered_limit (T : ∀ j, Set (Set (F.obj j)))
       rw [dif_pos he, ← Set.preimage_comp]
       apply congrFun
       apply congrArg
-      rw [← coe_comp, D.w]
+      erw [← coe_comp, D.w] -- now `erw` after #13170
       rfl
 #align Top.is_topological_basis_cofiltered_limit TopCat.isTopologicalBasis_cofiltered_limit
 
diff --git a/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/Mathlib/Topology/Category/TopCat/Limits/Products.lean
index a0e03bd0d5591..d078260198705 100644
--- a/Mathlib/Topology/Category/TopCat/Limits/Products.lean
+++ b/Mathlib/Topology/Category/TopCat/Limits/Products.lean
@@ -8,6 +8,7 @@ import Mathlib.Topology.Category.TopCat.Limits.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.Products
 import Mathlib.CategoryTheory.Limits.ConcreteCategory
 import Mathlib.Data.Set.Subsingleton
+import Mathlib.Tactic.CategoryTheory.Elementwise
 
 #align_import topology.category.Top.limits.products from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
 
@@ -72,14 +73,12 @@ theorem piIsoPi_inv_π {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) :
     (piIsoPi α).inv ≫ Pi.π α i = piπ α i := by simp [piIsoPi]
 #align Top.pi_iso_pi_inv_π TopCat.piIsoPi_inv_π
 
-@[simp]
 theorem piIsoPi_inv_π_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) (x : ∀ i, α i) :
     (Pi.π α i : _) ((piIsoPi α).inv x) = x i :=
   ConcreteCategory.congr_hom (piIsoPi_inv_π α i) x
 #align Top.pi_iso_pi_inv_π_apply TopCat.piIsoPi_inv_π_apply
 
 -- Porting note: needing the type ascription on `∏ᶜ α : TopCat.{max v u}` is unfortunate.
-@[simp]
 theorem piIsoPi_hom_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι)
     (x : (∏ᶜ α : TopCat.{max v u})) : (piIsoPi α).hom x i = (Pi.π α i : _) x := by
   have := piIsoPi_inv_π α i
@@ -129,13 +128,11 @@ theorem sigmaIsoSigma_hom_ι {ι : Type v} (α : ι → TopCat.{max v u}) (i : 
     Sigma.ι α i ≫ (sigmaIsoSigma α).hom = sigmaι α i := by simp [sigmaIsoSigma]
 #align Top.sigma_iso_sigma_hom_ι TopCat.sigmaIsoSigma_hom_ι
 
-@[simp]
 theorem sigmaIsoSigma_hom_ι_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) (x : α i) :
     (sigmaIsoSigma α).hom ((Sigma.ι α i : _) x) = Sigma.mk i x :=
   ConcreteCategory.congr_hom (sigmaIsoSigma_hom_ι α i) x
 #align Top.sigma_iso_sigma_hom_ι_apply TopCat.sigmaIsoSigma_hom_ι_apply
 
-@[simp]
 theorem sigmaIsoSigma_inv_apply {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) (x : α i) :
     (sigmaIsoSigma α).inv ⟨i, x⟩ = (Sigma.ι α i : _) x := by
   rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ← comp_app, Iso.hom_inv_id,
@@ -219,7 +216,6 @@ theorem prodIsoProd_hom_snd (X Y : TopCat.{u}) :
 #align Top.prod_iso_prod_hom_snd TopCat.prodIsoProd_hom_snd
 
 -- Porting note: need to force Lean to coerce X × Y to a type
-@[simp]
 theorem prodIsoProd_hom_apply {X Y : TopCat.{u}} (x : ↑ (X ⨯ Y)) :
     (prodIsoProd X Y).hom x = ((Limits.prod.fst : X ⨯ Y ⟶ _) x,
     (Limits.prod.snd : X ⨯ Y ⟶ _) x) := by
@@ -257,27 +253,36 @@ theorem range_prod_map {W X Y Z : TopCat.{u}} (f : W ⟶ Y) (g : X ⟶ Z) :
   ext x
   constructor
   · rintro ⟨y, rfl⟩
-    simp_rw [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range, ← comp_apply, Limits.prod.map_fst,
-      Limits.prod.map_snd, comp_apply, exists_apply_eq_apply, and_self_iff]
+    simp_rw [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range]
+    -- sizable changes in this proof after #13170
+    erw  [← comp_apply, ← comp_apply]
+    simp_rw [Limits.prod.map_fst,
+      Limits.prod.map_snd, comp_apply]
+    exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩
   · rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
     use (prodIsoProd W X).inv (x₁, x₂)
+    change (forget TopCat).map _ _ = _
     apply Concrete.limit_ext
     rintro ⟨⟨⟩⟩
-    · simp only [← comp_apply, Category.assoc]
-      erw [Limits.prod.map_fst]
-      rw [TopCat.prodIsoProd_inv_fst_assoc,TopCat.comp_app]
+    · change limit.π (pair Y Z) _ ((prod.map f g) _) = _
+      erw [← comp_apply, Limits.prod.map_fst]
+      change (_ ≫ _ ≫ f) _ = _
+      erw [TopCat.prodIsoProd_inv_fst_assoc,TopCat.comp_app]
       exact hx₁
-    · simp only [← comp_apply, Category.assoc]
-      erw [Limits.prod.map_snd]
-      rw [TopCat.prodIsoProd_inv_snd_assoc,TopCat.comp_app]
+    · change limit.π (pair Y Z) _ ((prod.map f g) _) = _
+      erw [← comp_apply, Limits.prod.map_snd]
+      change (_ ≫ _ ≫ g) _ = _
+      erw [TopCat.prodIsoProd_inv_snd_assoc,TopCat.comp_app]
       exact hx₂
 #align Top.range_prod_map TopCat.range_prod_map
 
 theorem inducing_prod_map {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Inducing f)
     (hg : Inducing g) : Inducing (Limits.prod.map f g) := by
   constructor
-  simp_rw [prod_topology, induced_inf, induced_compose, ← coe_comp, prod.map_fst, prod.map_snd,
-    coe_comp, ← induced_compose (g := f), ← induced_compose (g := g), ← hf.induced, ← hg.induced]
+  simp_rw [topologicalSpace_coe, prod_topology, induced_inf, induced_compose, ← coe_comp,
+    prod.map_fst, prod.map_snd, coe_comp, ← induced_compose (g := f), ← induced_compose (g := g)]
+  erw [← hf.induced, ← hg.induced] -- now `erw` after #13170
+  rfl -- `rfl` was not needed before #13170
 #align Top.inducing_prod_map TopCat.inducing_prod_map
 
 theorem embedding_prod_map {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Embedding f)
@@ -327,10 +332,9 @@ theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) :
         (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inl,
           (homeoOfIso <| h.coconePointUniqueUpToIso
             (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inr, ?_⟩
-      erw [Set.range_comp, ← eq_compl_iff_isCompl, coe_comp, coe_comp, Set.range_comp _ Sum.inr,
+      erw [Set.range_comp, ← eq_compl_iff_isCompl, Set.range_comp _ Sum.inr,
         ← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso
             (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr, Set.image_comp]
-      aesop
     · rintro ⟨h₁, h₂, h₃⟩
       have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr := by
         rw [eq_compl_iff_isCompl.mpr h₃.symm]
@@ -377,7 +381,9 @@ theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) :
         ext x
         refine (dif_pos ?_).trans ?_
         · exact ⟨x, rfl⟩
-        · dsimp; conv_lhs => erw [Equiv.ofInjective_symm_apply]
+        · dsimp
+          conv_lhs => erw [Equiv.ofInjective_symm_apply]
+          rfl -- `rfl` was not needed here before #13170
       · intro T f g
         ext x
         refine (dif_neg ?_).trans ?_
diff --git a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
index f634d39ee3ac2..bdc1da9aa8e18 100644
--- a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
+++ b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
@@ -38,7 +38,7 @@ abbrev pullbackFst (f : X ⟶ Z) (g : Y ⟶ Z) : TopCat.of { p : X × Y // f p.1
     apply Continuous.comp <;> set_option tactic.skipAssignedInstances false in continuity⟩
 #align Top.pullback_fst TopCat.pullbackFst
 
-@[simp] lemma pullbackFst_apply (f : X ⟶ Z) (g : Y ⟶ Z) (x) : pullbackFst f g x = x.1.1 := rfl
+lemma pullbackFst_apply (f : X ⟶ Z) (g : Y ⟶ Z) (x) : pullbackFst f g x = x.1.1 := rfl
 
 /-- The second projection from the pullback. -/
 abbrev pullbackSnd (f : X ⟶ Z) (g : Y ⟶ Z) : TopCat.of { p : X × Y // f p.1 = g p.2 } ⟶ Y :=
@@ -46,7 +46,7 @@ abbrev pullbackSnd (f : X ⟶ Z) (g : Y ⟶ Z) : TopCat.of { p : X × Y // f p.1
     apply Continuous.comp <;> set_option tactic.skipAssignedInstances false in continuity⟩
 #align Top.pullback_snd TopCat.pullbackSnd
 
-@[simp] lemma pullbackSnd_apply (f : X ⟶ Z) (g : Y ⟶ Z) (x) : pullbackSnd f g x = x.1.2 := rfl
+lemma pullbackSnd_apply (f : X ⟶ Z) (g : Y ⟶ Z) (x) : pullbackSnd f g x = x.1.2 := rfl
 
 /-- The explicit pullback cone of `X, Y` given by `{ p : X × Y // f p.1 = g p.2 }`. -/
 def pullbackCone (f : X ⟶ Z) (g : Y ⟶ Z) : PullbackCone f g :=
@@ -105,7 +105,6 @@ theorem pullbackIsoProdSubtype_inv_fst (f : X ⟶ Z) (g : Y ⟶ Z) :
   simp [pullbackCone, pullbackIsoProdSubtype]
 #align Top.pullback_iso_prod_subtype_inv_fst TopCat.pullbackIsoProdSubtype_inv_fst
 
-@[simp]
 theorem pullbackIsoProdSubtype_inv_fst_apply (f : X ⟶ Z) (g : Y ⟶ Z)
     (x : { p : X × Y // f p.1 = g p.2 }) :
     (pullback.fst : pullback f g ⟶ _) ((pullbackIsoProdSubtype f g).inv x) = (x : X × Y).fst :=
@@ -118,7 +117,6 @@ theorem pullbackIsoProdSubtype_inv_snd (f : X ⟶ Z) (g : Y ⟶ Z) :
   simp [pullbackCone, pullbackIsoProdSubtype]
 #align Top.pullback_iso_prod_subtype_inv_snd TopCat.pullbackIsoProdSubtype_inv_snd
 
-@[simp]
 theorem pullbackIsoProdSubtype_inv_snd_apply (f : X ⟶ Z) (g : Y ⟶ Z)
     (x : { p : X × Y // f p.1 = g p.2 }) :
     (pullback.snd : pullback f g ⟶ _) ((pullbackIsoProdSubtype f g).inv x) = (x : X × Y).snd :=
@@ -136,7 +134,6 @@ theorem pullbackIsoProdSubtype_hom_snd (f : X ⟶ Z) (g : Y ⟶ Z) :
 #align Top.pullback_iso_prod_subtype_hom_snd TopCat.pullbackIsoProdSubtype_hom_snd
 
 -- Porting note: why do I need to tell Lean to coerce pullback to a type
-@[simp]
 theorem pullbackIsoProdSubtype_hom_apply {f : X ⟶ Z} {g : Y ⟶ Z}
     (x : ConcreteCategory.forget.obj (pullback f g)) :
     (pullbackIsoProdSubtype f g).hom x =
@@ -164,14 +161,14 @@ theorem range_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :
   ext x
   constructor
   · rintro ⟨y, rfl⟩
-    simp only [← comp_apply, Set.mem_setOf_eq]
-    congr 1
+    change (_ ≫ _ ≫ f) _ = (_ ≫ _ ≫ g) _ -- new `change` after #13170
     simp [pullback.condition]
   · rintro (h : f (_, _).1 = g (_, _).2)
     use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩
+    change (forget TopCat).map _ _ = _ -- new `change` after #13170
     apply Concrete.limit_ext
     rintro ⟨⟨⟩⟩ <;>
-    rw [← comp_apply, ← comp_apply, limit.lift_π] <;>
+    erw [← comp_apply, ← comp_apply, limit.lift_π] <;> -- now `erw` after #13170
     -- This used to be `simp` before leanprover/lean4#2644
     aesop_cat
 #align Top.range_pullback_to_prod TopCat.range_pullback_to_prod
@@ -203,7 +200,7 @@ def pullbackHomeoPreimage
 
 theorem inducing_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) :
     Inducing <| ⇑(prod.lift pullback.fst pullback.snd : pullback f g ⟶ X ⨯ Y) :=
-  ⟨by simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]⟩
+  ⟨by simp [topologicalSpace_coe, prod_topology, pullback_topology, induced_compose, ← coe_comp]⟩
 #align Top.inducing_pullback_to_prod TopCat.inducing_pullback_to_prod
 
 theorem embedding_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) :
@@ -221,48 +218,58 @@ theorem range_pullback_map {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶
   ext
   constructor
   · rintro ⟨y, rfl⟩
-    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range, ← comp_apply, limit.lift_π,
-      PullbackCone.mk_pt, PullbackCone.mk_π_app]
-    simp only [comp_apply, exists_apply_eq_apply, and_self]
+    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range]
+    erw [← comp_apply, ← comp_apply] -- now `erw` after #13170
+    simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, comp_apply]
+    exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩
   rintro ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩
   have : f₁ x₁ = f₂ x₂ := by
     apply (TopCat.mono_iff_injective _).mp H₃
-    simp only [← comp_apply, eq₁, eq₂]
-    simp only [comp_apply, hx₁, hx₂]
-    simp only [← comp_apply, pullback.condition]
+    erw [← comp_apply, eq₁, ← comp_apply, eq₂, -- now `erw` after #13170
+      comp_apply, comp_apply, hx₁, hx₂, ← comp_apply, pullback.condition]
+    rfl -- `rfl` was not needed before #13170
   use (pullbackIsoProdSubtype f₁ f₂).inv ⟨⟨x₁, x₂⟩, this⟩
+  change (forget TopCat).map _ _ = _
   apply Concrete.limit_ext
   rintro (_ | _ | _) <;>
-  simp only [← comp_apply, Category.assoc, limit.lift_π, PullbackCone.mk_π_app_one]
-  · simp only [cospan_one, pullbackIsoProdSubtype_inv_fst_assoc, comp_apply,
-      pullbackFst_apply, hx₁]
+  erw [← comp_apply, ← comp_apply] -- now `erw` after #13170
+  simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app_one]
+  · simp only [cospan_one, pullbackIsoProdSubtype_inv_fst_assoc, comp_apply]
+    erw [pullbackFst_apply, hx₁]
     rw [← limit.w _ WalkingCospan.Hom.inl, cospan_map_inl, comp_apply (g := g₁)]
-  · simp [hx₁]
-  · simp [hx₂]
+    rfl -- `rfl` was not needed before #13170
+  · simp only [cospan_left, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
+      pullbackIsoProdSubtype_inv_fst_assoc, comp_apply]
+    erw [hx₁] -- now `erw` after #13170
+    rfl -- `rfl` was not needed before #13170
+  · simp only [cospan_right, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
+      pullbackIsoProdSubtype_inv_snd_assoc, comp_apply]
+    erw [hx₂] -- now `erw` after #13170
+    rfl -- `rfl` was not needed before #13170
 #align Top.range_pullback_map TopCat.range_pullback_map
 
 theorem pullback_fst_range {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :
     Set.range (pullback.fst : pullback f g ⟶ _) = { x : X | ∃ y : Y, f x = g y } := by
   ext x
   constructor
-  · rintro ⟨y, rfl⟩
+  · rintro ⟨(y : (forget TopCat).obj _), rfl⟩
     use (pullback.snd : pullback f g ⟶ _) y
     exact ConcreteCategory.congr_hom pullback.condition y
   · rintro ⟨y, eq⟩
     use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
-    simp
+    rw [pullbackIsoProdSubtype_inv_fst_apply]
 #align Top.pullback_fst_range TopCat.pullback_fst_range
 
 theorem pullback_snd_range {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :
     Set.range (pullback.snd : pullback f g ⟶ _) = { y : Y | ∃ x : X, f x = g y } := by
   ext y
   constructor
-  · rintro ⟨x, rfl⟩
+  · rintro ⟨(x : (forget TopCat).obj _), rfl⟩
     use (pullback.fst : pullback f g ⟶ _) x
     exact ConcreteCategory.congr_hom pullback.condition x
   · rintro ⟨x, eq⟩
     use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
-    simp
+    rw [pullbackIsoProdSubtype_inv_snd_apply]
 #align Top.pullback_snd_range TopCat.pullback_snd_range
 
 /-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are embeddings,
@@ -401,11 +408,17 @@ theorem pullback_snd_image_fst_preimage (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set X)
       g ⁻¹' (f '' U) := by
   ext x
   constructor
-  · rintro ⟨y, hy, rfl⟩
+  · rintro ⟨(y : (forget TopCat).obj _), hy, rfl⟩
     exact
       ⟨(pullback.fst : pullback f g ⟶ _) y, hy, ConcreteCategory.congr_hom pullback.condition y⟩
   · rintro ⟨y, hy, eq⟩
-    exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, by simpa, by simp⟩
+  -- next 5 lines were
+  -- `exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, by simpa, by simp⟩` before #13170
+    refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩
+    · simp only [coe_of, Set.mem_preimage]
+      convert hy
+      erw [pullbackIsoProdSubtype_inv_fst_apply]
+    · rw [pullbackIsoProdSubtype_inv_snd_apply]
 #align Top.pullback_snd_image_fst_preimage TopCat.pullback_snd_image_fst_preimage
 
 theorem pullback_fst_image_snd_preimage (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set Y) :
@@ -413,12 +426,19 @@ theorem pullback_fst_image_snd_preimage (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set Y)
       f ⁻¹' (g '' U) := by
   ext x
   constructor
-  · rintro ⟨y, hy, rfl⟩
+  · rintro ⟨(y : (forget TopCat).obj _), hy, rfl⟩
     exact
       ⟨(pullback.snd : pullback f g ⟶ _) y, hy,
         (ConcreteCategory.congr_hom pullback.condition y).symm⟩
   · rintro ⟨y, hy, eq⟩
-    exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq.symm⟩, by simpa, by simp⟩
+    -- next 5 lines were
+    -- `exact ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq.symm⟩, by simpa, by simp⟩`
+    -- before #13170
+    refine ⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq.symm⟩, ?_, ?_⟩
+    · simp only [coe_of, Set.mem_preimage]
+      convert hy
+      erw [pullbackIsoProdSubtype_inv_snd_apply]
+    · rw [pullbackIsoProdSubtype_inv_fst_apply]
 #align Top.pullback_fst_image_snd_preimage TopCat.pullback_fst_image_snd_preimage
 
 end Pullback
diff --git a/Mathlib/Topology/Category/UniformSpace.lean b/Mathlib/Topology/Category/UniformSpace.lean
index 64478175c7338..22f8e68d49d50 100644
--- a/Mathlib/Topology/Category/UniformSpace.lean
+++ b/Mathlib/Topology/Category/UniformSpace.lean
@@ -198,6 +198,8 @@ noncomputable def extensionHom {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
 instance (X : UniformSpaceCat) : UniformSpace ((forget _).obj X) :=
   show UniformSpace X from inferInstance
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike in
 @[simp]
 theorem extensionHom_val {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
     (f : X ⟶ (forget₂ _ _).obj Y) (x) : (extensionHom f) x = Completion.extension f x :=
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
index 099ade96791df..d32df9f2adcd4 100644
--- a/Mathlib/Topology/Gluing.lean
+++ b/Mathlib/Topology/Gluing.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.GlueData
 import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
 import Mathlib.Topology.Category.TopCat.Opens
 import Mathlib.Tactic.Generalize
+import Mathlib.CategoryTheory.Elementwise
 
 #align_import topology.gluing from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1"
 
@@ -131,13 +132,16 @@ set_option linter.uppercaseLean3 false in
 theorem rel_equiv : Equivalence D.Rel :=
   ⟨fun x => Or.inl (refl x), by
     rintro a b (⟨⟨⟩⟩ | ⟨x, e₁, e₂⟩)
-    exacts [Or.inl rfl, Or.inr ⟨D.t _ _ x, by simp [e₁, e₂]⟩], by
+    exacts [Or.inl rfl, Or.inr ⟨D.t _ _ x, e₂, by erw [← e₁, D.t_inv_apply]⟩], by
+     -- previous line now `erw` after #13170
     rintro ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ (⟨⟨⟩⟩ | ⟨x, e₁, e₂⟩)
     · exact id
     rintro (⟨⟨⟩⟩ | ⟨y, e₃, e₄⟩)
     · exact Or.inr ⟨x, e₁, e₂⟩
     let z := (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv ⟨⟨_, _⟩, e₂.trans e₃.symm⟩
-    have eq₁ : (D.t j i) ((pullback.fst : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x := by simp [z]
+    have eq₁ : (D.t j i) ((pullback.fst : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x := by
+      dsimp only [coe_of, z]
+      erw [pullbackIsoProdSubtype_inv_fst_apply, D.t_inv_apply]-- now `erw` after #13170
     have eq₂ : (pullback.snd : _ ⟶ D.V _) z = y := pullbackIsoProdSubtype_inv_snd_apply _ _ _
     clear_value z
     right
@@ -215,9 +219,10 @@ theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) :
     obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ :=
       (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x
     unfold InvImage MultispanIndex.fstSigmaMap MultispanIndex.sndSigmaMap
-    simp only [forget_map_eq_coe, Opens.inclusion_apply, TopCat.comp_app, sigmaIsoSigma_inv_apply,
-      Cofan.mk_ι_app]
-    rw [← comp_apply, colimit.ι_desc, ← comp_apply, colimit.ι_desc]
+    simp only [forget_map_eq_coe]
+    erw [TopCat.comp_app, sigmaIsoSigma_inv_apply, ← comp_apply, ← comp_apply,
+      colimit.ι_desc_assoc, ← comp_apply, ← comp_apply, colimit.ι_desc_assoc]
+      -- previous line now `erw` after #13170
     erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]
     exact Or.inr ⟨y, ⟨rfl, rfl⟩⟩
   · rintro (⟨⟨⟩⟩ | ⟨z, e₁, e₂⟩)
@@ -225,7 +230,8 @@ theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) :
     dsimp only at *
     -- Porting note: there were `subst e₁` and `subst e₂`, instead of the `rw`
     rw [← e₁, ← e₂] at *
-    simp
+    erw [D.glue_condition_apply] -- now `erw` after #13170
+    rfl -- now `rfl` after #13170
 set_option linter.uppercaseLean3 false in
 #align Top.glue_data.ι_eq_iff_rel TopCat.GlueData.ι_eq_iff_rel
 
@@ -263,7 +269,9 @@ theorem image_inter (i j : D.J) :
       substs eq₁
       exact ⟨y, by simp [e₁]⟩
   · rintro ⟨x, hx⟩
-    exact ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), by simp [← hx]⟩⟩
+    refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩
+    erw [D.glue_condition_apply] -- now `erw` after #13170
+    exact hx
 set_option linter.uppercaseLean3 false in
 #align Top.glue_data.image_inter TopCat.GlueData.image_inter
 
@@ -279,8 +287,11 @@ theorem preimage_image_eq_image (i j : D.J) (U : Set (𝖣.U i)) :
   have : D.f _ _ ⁻¹' (𝖣.ι j ⁻¹' (𝖣.ι i '' U)) = (D.t j i ≫ D.f _ _) ⁻¹' U := by
     ext x
     conv_rhs => rw [← Set.preimage_image_eq U (D.ι_injective _)]
-    generalize 𝖣.ι i '' U = U'
-    simp
+    generalize 𝖣.ι i '' U = U' -- next 4 lines were `simp` before #13170
+    simp only [GlueData.diagram_l, GlueData.diagram_r, Set.mem_preimage, coe_comp,
+      Function.comp_apply]
+    erw [D.glue_condition_apply]
+    rfl
   rw [← this, Set.image_preimage_eq_inter_range]
   symm
   apply Set.inter_eq_self_of_subset_left
@@ -396,7 +407,7 @@ def mk' (h : MkCore.{u}) : TopCat.GlueData where
     exact (h.V_id i).symm ▸ IsIso.of_iso (Opens.inclusionTopIso (h.U i))
   f_open := fun i j : h.J => (h.V i j).openEmbedding
   t := h.t
-  t_id i := by ext; rw [h.t_id]; rfl
+  t_id i := by ext; erw [h.t_id]; rfl  -- now `erw` after #13170
   t' := h.t'
   t_fac i j k := by
     delta MkCore.t'
@@ -414,7 +425,7 @@ def mk' (h : MkCore.{u}) : TopCat.GlueData where
     -- The next 9 tactics (up to `convert ...` were a single `rw` before leanprover/lean4#2644
     -- rw [comp_app, ContinuousMap.coe_mk, comp_app, id_app, ContinuousMap.coe_mk, Subtype.mk_eq_mk,
     --   Prod.mk.inj_iff, Subtype.mk_eq_mk, Subtype.ext_iff, and_self_iff]
-    rw [comp_app] --, comp_app, id_app]
+    erw [comp_app] --, comp_app, id_app] -- now `erw` after #13170
     -- erw [ContinuousMap.coe_mk]
     conv_lhs => erw [ContinuousMap.coe_mk]
     erw [id_app]
diff --git a/Mathlib/Topology/Order/Category/AlexDisc.lean b/Mathlib/Topology/Order/Category/AlexDisc.lean
index 886568b8cb136..b09f41180fa6d 100644
--- a/Mathlib/Topology/Order/Category/AlexDisc.lean
+++ b/Mathlib/Topology/Order/Category/AlexDisc.lean
@@ -45,6 +45,9 @@ def of (α : Type*) [TopologicalSpace α] [AlexandrovDiscrete α] : AlexDisc :=
 @[simp] lemma forgetToTop_of (α : Type*) [TopologicalSpace α] [AlexandrovDiscrete α] :
   (forget₂ AlexDisc TopCat).obj (of α) = TopCat.of α := rfl
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 /-- Constructs an equivalence between preorders from an order isomorphism between them. -/
 @[simps]
 def Iso.mk {α β : AlexDisc} (e : α ≃ₜ β) : α ≅ β where
diff --git a/Mathlib/Topology/Order/Category/FrameAdjunction.lean b/Mathlib/Topology/Order/Category/FrameAdjunction.lean
index 5ad6a5c6815ca..9d5db86970bb8 100644
--- a/Mathlib/Topology/Order/Category/FrameAdjunction.lean
+++ b/Mathlib/Topology/Order/Category/FrameAdjunction.lean
@@ -76,6 +76,9 @@ lemma isOpen_iff (U : Set (PT L)) : IsOpen U ↔ ∃ u : L, {x | x u} = U := Iff
 
 end PT
 
+-- This was a global instance prior to #13170. We may experiment with removing it.
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 /-- The covariant functor `pt` from the category of locales to the category of
 topological spaces, which sends a locale `L` to the topological space `PT L` of homomorphisms
 from `L` to `Prop` and a locale homomorphism `f` to a continuous function between the spaces
diff --git a/Mathlib/Topology/Sheaves/LocallySurjective.lean b/Mathlib/Topology/Sheaves/LocallySurjective.lean
index 4e5ea9da853ce..87d2982f5d779 100644
--- a/Mathlib/Topology/Sheaves/LocallySurjective.lean
+++ b/Mathlib/Topology/Sheaves/LocallySurjective.lean
@@ -31,6 +31,9 @@ We prove that these are equivalent.
 
 universe v u
 
+
+attribute [local instance] CategoryTheory.ConcreteCategory.instFunLike
+
 noncomputable section
 
 open CategoryTheory
diff --git a/Mathlib/Topology/Sheaves/Operations.lean b/Mathlib/Topology/Sheaves/Operations.lean
index 9905500b9c095..ef8bec88bcfe2 100644
--- a/Mathlib/Topology/Sheaves/Operations.lean
+++ b/Mathlib/Topology/Sheaves/Operations.lean
@@ -37,7 +37,7 @@ namespace Presheaf
 
 variable {X : TopCat.{w}} {C : Type u} [Category.{v} C] [ConcreteCategory C]
 
-attribute [local instance 1000] ConcreteCategory.hasCoeToSort
+attribute [local instance 1000] ConcreteCategory.hasCoeToSort ConcreteCategory.instFunLike
 
 /-- A subpresheaf with a submonoid structure on each of the components. -/
 structure SubmonoidPresheaf [∀ X : C, MulOneClass X] [∀ X Y : C, MonoidHomClass (X ⟶ Y) X Y]
diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean
index a2325f991f19c..2f56bc3f1ba64 100644
--- a/Mathlib/Topology/Sheaves/Stalks.lean
+++ b/Mathlib/Topology/Sheaves/Stalks.lean
@@ -109,6 +109,7 @@ set_option linter.uppercaseLean3 false in
 #align Top.presheaf.germ_res TopCat.Presheaf.germ_res
 
 -- Porting note: `@[elementwise]` did not generate the best lemma when applied to `germ_res`
+attribute [local instance] ConcreteCategory.instFunLike in
 theorem germ_res_apply (F : X.Presheaf C) {U V : Opens X} (i : U ⟶ V) (x : U) [ConcreteCategory C]
     (s) : germ F x (F.map i.op s) = germ F (i x) s := by rw [← comp_apply, germ_res]
 set_option linter.uppercaseLean3 false in
@@ -385,9 +386,7 @@ section Concrete
 variable {C}
 variable [ConcreteCategory.{v} C]
 
-attribute [local instance] ConcreteCategory.hasCoeToSort
--- Porting note: The following does not seem to be needed.
--- ConcreteCategory.hasCoeToFun
+attribute [local instance] ConcreteCategory.hasCoeToSort ConcreteCategory.instFunLike
 
 -- Porting note (#11215): TODO: @[ext] attribute only applies to structures or lemmas proving x = y
 -- @[ext]