feat: change ConcreteCategory.hasCoeToFun to FunLike (#4693)

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -98,6 +98,12 @@ theorem coe_of (R : Type u) [Semiring R] : (SemiRingCat.of R : Type u) = R :=
 set_option linter.uppercaseLean3 false in
 #align SemiRing.coe_of SemiRingCat.coe_of
 
+@[simp]
+lemma RingEquiv_coe_eq {X Y : Type _} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
+    (@FunLike.coe (SemiRingCat.of X ⟶ SemiRingCat.of Y) _ (fun _ => (forget SemiRingCat).obj _)
+      ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
+  rfl
+
 instance : Inhabited SemiRingCat :=
   ⟨of PUnit⟩
 
@@ -131,6 +137,9 @@ theorem ofHom_apply {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x
 set_option linter.uppercaseLean3 false in
 #align SemiRing.of_hom_apply SemiRingCat.ofHom_apply
 
+/--
+Ring equivalence are isomorphisms in category of semirings
+-/
 @[simps]
 def _root_.RingEquiv.toSemiRingCatIso [Semiring X] [Semiring Y] (e : X ≃+* Y) :
     SemiRingCat.of X ≅ SemiRingCat.of Y where
@@ -217,6 +226,12 @@ theorem coe_of (R : Type u) [Ring R] : (RingCat.of R : Type u) = R :=
 set_option linter.uppercaseLean3 false in
 #align Ring.coe_of RingCat.coe_of
 
+@[simp]
+lemma RingEquiv_coe_eq {X Y : Type _} [Ring X] [Ring Y] (e : X ≃+* Y) :
+    (@FunLike.coe (RingCat.of X ⟶ RingCat.of Y) _ (fun _ => (forget RingCat).obj _)
+      ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
+  rfl
+
 instance hasForgetToSemiRingCat : HasForget₂ RingCat SemiRingCat :=
   BundledHom.forget₂ _ _
 set_option linter.uppercaseLean3 false in
@@ -239,7 +254,7 @@ def CommSemiRingCat : Type (u + 1) :=
 set_option linter.uppercaseLean3 false in
 #align CommSemiRing CommSemiRingCat
 
-namespace CommSemiRing
+namespace CommSemiRingCat
 
 instance : BundledHom.ParentProjection @CommSemiring.toSemiring :=
   ⟨⟩
@@ -276,13 +291,20 @@ lemma ext {X Y : CommSemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f
 def of (R : Type u) [CommSemiring R] : CommSemiRingCat :=
   Bundled.of R
 set_option linter.uppercaseLean3 false in
-#align CommSemiRing.of CommSemiRing.of
+#align CommSemiRing.of CommSemiRingCat.of
 
 /-- Typecheck a `RingHom` as a morphism in `CommSemiRingCat`. -/
 def ofHom {R S : Type u} [CommSemiring R] [CommSemiring S] (f : R →+* S) : of R ⟶ of S :=
   f
 set_option linter.uppercaseLean3 false in
-#align CommSemiRing.of_hom CommSemiRing.ofHom
+#align CommSemiRing.of_hom CommSemiRingCat.ofHom
+
+@[simp]
+lemma RingEquiv_coe_eq {X Y : Type _} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
+    (@FunLike.coe (CommSemiRingCat.of X ⟶ CommSemiRingCat.of Y) _
+      (fun _ => (forget CommSemiRingCat).obj _)
+      ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
+  rfl
 
 -- Porting note: I think this is now redundant.
 -- @[simp]
@@ -299,25 +321,27 @@ instance (R : CommSemiRingCat) : CommSemiring R :=
   R.str
 
 @[simp]
-theorem coe_of (R : Type u) [CommSemiring R] : (CommSemiRing.of R : Type u) = R :=
+theorem coe_of (R : Type u) [CommSemiring R] : (CommSemiRingCat.of R : Type u) = R :=
   rfl
 set_option linter.uppercaseLean3 false in
-#align CommSemiRing.coe_of CommSemiRing.coe_of
+#align CommSemiRing.coe_of CommSemiRingCat.coe_of
 
 instance hasForgetToSemiRingCat : HasForget₂ CommSemiRingCat SemiRingCat :=
   BundledHom.forget₂ _ _
 set_option linter.uppercaseLean3 false in
-#align CommSemiRing.has_forget_to_SemiRing CommSemiRing.hasForgetToSemiRingCat
+#align CommSemiRing.has_forget_to_SemiRing CommSemiRingCat.hasForgetToSemiRingCat
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 instance hasForgetToCommMonCat : HasForget₂ CommSemiRingCat CommMonCat :=
   HasForget₂.mk' (fun R : CommSemiRingCat => CommMonCat.of R) (fun R => rfl)
     -- Porting note: `(_ := _)` trick
     (fun {R₁ R₂} f => RingHom.toMonoidHom (α := R₁) (β := R₂) f) (by rfl)
 set_option linter.uppercaseLean3 false in
-#align CommSemiRing.has_forget_to_CommMon CommSemiRing.hasForgetToCommMonCat
-
+#align CommSemiRing.has_forget_to_CommMon CommSemiRingCat.hasForgetToCommMonCat
 
+/--
+Ring equivalence are isomorphisms in category of commutative semirings
+-/
 @[simps]
 def _root_.RingEquiv.toCommSemiRingCatIso [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
     SemiRingCat.of X ≅ SemiRingCat.of Y where
@@ -331,7 +355,7 @@ instance forgetReflectIsos : ReflectsIsomorphisms (forget CommSemiRingCat) where
     let e : X ≃+* Y := { ff, i.toEquiv with }
     exact ⟨(IsIso.of_iso e.toSemiRingCatIso).1⟩
 
-end CommSemiRing
+end CommSemiRingCat
 
 /-- The category of commutative rings. -/
 def CommRingCat : Type (u + 1) :=
@@ -384,6 +408,12 @@ def ofHom {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : of R ⟶ of
 set_option linter.uppercaseLean3 false in
 #align CommRing.of_hom CommRingCat.ofHom
 
+@[simp]
+lemma RingEquiv_coe_eq {X Y : Type _} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
+    (@FunLike.coe (CommRingCat.of X ⟶ CommRingCat.of Y) _ (fun _ => (forget CommRingCat).obj _)
+      ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
+  rfl
+
 -- Porting note: I think this is now redundant.
 -- @[simp]
 -- theorem ofHom_apply {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (x : R) :
@@ -411,7 +441,7 @@ set_option linter.uppercaseLean3 false in
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
 instance hasForgetToCommSemiRingCat : HasForget₂ CommRingCat CommSemiRingCat :=
-  HasForget₂.mk' (fun R : CommRingCat => CommSemiRing.of R) (fun R => rfl)
+  HasForget₂.mk' (fun R : CommRingCat => CommSemiRingCat.of R) (fun R => rfl)
     (fun {R₁ R₂} f => f) (by rfl)
 set_option linter.uppercaseLean3 false in
 #align CommRing.has_forget_to_CommSemiRing CommRingCat.hasForgetToCommSemiRingCat
@@ -475,15 +505,17 @@ def commRingCatIsoToRingEquiv {X Y : CommRingCat} (i : X ≅ Y) : X ≃+* Y
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.CommRing_iso_to_ring_equiv CategoryTheory.Iso.commRingCatIsoToRingEquiv
 
-@[simp]
+-- Porting note : make this high priority to short circuit simplifier
+@[simp (high)]
 theorem commRingIsoToRingEquiv_toRingHom {X Y : CommRingCat} (i : X ≅ Y) :
     i.commRingCatIsoToRingEquiv.toRingHom = i.hom := by
   ext
   rfl
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.CommRing_iso_to_ring_equiv_to_ring_hom CategoryTheory.Iso.commRingIsoToRingEquiv_toRingHom
 
-@[simp]
+-- Porting note : make this high priority to short circuit simplifier
+@[simp (high)]
 theorem commRingIsoToRingEquiv_symm_toRingHom {X Y : CommRingCat} (i : X ≅ Y) :
     i.commRingCatIsoToRingEquiv.symm.toRingHom = i.inv := by
   ext

Mathlib/Algebra/Category/Ring/FilteredColimits.lean

@@ -205,7 +205,7 @@ set_option linter.uppercaseLean3 false in
 
 /-- The bundled commutative semiring giving the filtered colimit of a diagram. -/
 def colimit : CommSemiRingCat.{max v u} :=
-  CommSemiRing.of <| R.{v, u} F
+  CommSemiRingCat.of <| R.{v, u} F
 set_option linter.uppercaseLean3 false in
 #align CommSemiRing.filtered_colimits.colimit CommSemiRingCat.FilteredColimits.colimit
 

Mathlib/Algebra/Category/Ring/Limits.lean

@@ -229,14 +229,14 @@ instance (F : J ⥤ CommSemiRingCatMax.{v, u}) :
   -- isomorphism is added manually since Lean can't see it, but even with this addition Lean can not
   -- see `CommSemiRingCat ⥤ SemiRingCat` reflects isomorphism, so this instance is also added.
   letI : ReflectsIsomorphisms (forget CommSemiRingCatMax.{v, u}) :=
-    CommSemiRing.forgetReflectIsos.{max v u}
+    CommSemiRingCat.forgetReflectIsos.{max v u}
   letI : ReflectsIsomorphisms
     (forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u}) :=
     CategoryTheory.reflectsIsomorphisms_forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u}
   let c : Cone F :=
-    { pt := CommSemiRing.of (Types.limitCone (F ⋙ forget _)).pt
+    { pt := CommSemiRingCat.of (Types.limitCone (F ⋙ forget _)).pt
       π :=
-        { app := fun j => CommSemiRing.ofHom <| SemiRingCat.limitπRingHom.{v, u} (J := J)
+        { app := fun j => CommSemiRingCat.ofHom <| SemiRingCat.limitπRingHom.{v, u} (J := J)
             (F ⋙ forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u}) j
           naturality := (SemiRingCat.HasLimits.limitCone.{v, u}
             (F ⋙ forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u})).π.naturality } }
@@ -246,7 +246,7 @@ instance (F : J ⥤ CommSemiRingCatMax.{v, u}) :
       makesLimit := by
         refine IsLimit.ofFaithful (forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u})
           (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _)
-          (fun s : Cone F => CommSemiRing.ofHom
+          (fun s : Cone F => CommSemiRingCat.ofHom
             ⟨⟨⟨_, Subtype.ext <| funext fun j => by exact (s.π.app j).map_one⟩,
             fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_mul x y⟩,
             Subtype.ext <| funext fun j => by exact (s.π.app j).map_zero,

Mathlib/Algebra/Ring/Equiv.lean

@@ -681,7 +681,7 @@ instance instCoeToRingHom : Coe (R ≃+* S) (R →+* S) :=
   ⟨RingEquiv.toRingHom⟩
 #align ring_equiv.has_coe_to_ring_hom RingEquiv.instCoeToRingHom
 
-theorem toRingHom_eq_coe (f : R ≃+* S) : f.toRingHom = ↑f :=
+@[simp] theorem toRingHom_eq_coe (f : R ≃+* S) : f.toRingHom = ↑f :=
   rfl
 #align ring_equiv.to_ring_hom_eq_coe RingEquiv.toRingHom_eq_coe
 
@@ -744,13 +744,13 @@ theorem toAddMonoidHom_refl : (RingEquiv.refl R).toAddMonoidHom = AddMonoidHom.i
   rfl
 #align ring_equiv.to_add_monoid_hom_refl RingEquiv.toAddMonoidHom_refl
 
-@[simp]
+-- Porting note : Now other `simp` can do this, so removed `simp` attribute
 theorem toRingHom_apply_symm_toRingHom_apply (e : R ≃+* S) :
     ∀ y : S, e.toRingHom (e.symm.toRingHom y) = y :=
   e.toEquiv.apply_symm_apply
 #align ring_equiv.to_ring_hom_apply_symm_to_ring_hom_apply RingEquiv.toRingHom_apply_symm_toRingHom_apply
 
-@[simp]
+-- Porting note : Now other `simp` can do this, so removed `simp` attribute
 theorem symm_toRingHom_apply_toRingHom_apply (e : R ≃+* S) :
     ∀ x : R, e.symm.toRingHom (e.toRingHom x) = x :=
   Equiv.symm_apply_apply e.toEquiv
@@ -762,14 +762,14 @@ theorem toRingHom_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
   rfl
 #align ring_equiv.to_ring_hom_trans RingEquiv.toRingHom_trans
 
-@[simp]
+-- Porting note : Now other `simp` can do this, so removed `simp` attribute
 theorem toRingHom_comp_symm_toRingHom (e : R ≃+* S) :
     e.toRingHom.comp e.symm.toRingHom = RingHom.id _ := by
   ext
   simp
 #align ring_equiv.to_ring_hom_comp_symm_to_ring_hom RingEquiv.toRingHom_comp_symm_toRingHom
 
-@[simp]
+-- Porting note : Now other `simp` can do this, so removed `simp` attribute
 theorem symm_toRingHom_comp_toRingHom (e : R ≃+* S) :
     e.symm.toRingHom.comp e.toRingHom = RingHom.id _ := by
   ext

Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean

@@ -302,19 +302,12 @@ theorem preimage_basicOpen {X Y : LocallyRingedSpace} (f : X ⟶ Y) {U : Opens Y
   ext x
   constructor
   · rintro ⟨⟨y, hyU⟩, hy : IsUnit _, rfl : y = _⟩
-    erw [RingedSpace.mem_basicOpen _ _ ⟨x, show x ∈ (Opens.map f.1.base).obj U from hyU⟩]
-    have eq1 := PresheafedSpace.stalkMap_germ_apply _ _
-      ⟨x, show x ∈ (Opens.map f.1.base).obj U from hyU⟩
-    dsimp at eq1
-    -- Porting note : `rw` and `erw` can't rewrite `stalkMap_germ_apply`
-    rw [← eq1]
+    erw [RingedSpace.mem_basicOpen _ _ ⟨x, show x ∈ (Opens.map f.1.base).obj U from hyU⟩,
+      ← PresheafedSpace.stalkMap_germ_apply]
     exact (PresheafedSpace.stalkMap f.1 _).isUnit_map hy
   · rintro ⟨y, hy : IsUnit _, rfl⟩
     erw [RingedSpace.mem_basicOpen _ _ ⟨f.1.base y.1, y.2⟩]
-    have eq1 := PresheafedSpace.stalkMap_germ_apply _ _ y
-    dsimp at eq1
-    -- Porting note : `rw` and `erw` can't rewrite `stalkMap_germ_apply`
-    rw [← eq1] at hy
+    erw [← PresheafedSpace.stalkMap_germ_apply] at hy
     exact (isUnit_map_iff (PresheafedSpace.stalkMap f.1 _) _).mp hy
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.LocallyRingedSpace.preimage_basic_open AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen

Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

@@ -404,8 +404,8 @@ def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v}
     refine' (F.obj (unop X)).presheaf.mapIso (eqToIso _)
     simp only [Functor.op_obj, unop_op, op_inj_iff, Opens.map_coe, SetLike.ext'_iff,
       Set.preimage_preimage]
-    simp_rw [← comp_app]
-    refine congr_arg (Set.preimage . U.1) (funext fun x => congr_fun ?_ x)
+    refine congr_arg (Set.preimage . U.1) (funext fun x => ?_)
+    erw [←comp_app]
     congr
     exact ι_preservesColimitsIso_inv (forget C) F (unop X)
   · intro X Y f

Mathlib/AlgebraicGeometry/RingedSpace.lean

@@ -78,12 +78,8 @@ theorem isUnit_res_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U)) (x :
     exact heq
   obtain ⟨W', hxW', i₁, i₂, heq'⟩ := X.presheaf.germ_eq x.1 hxW hxW _ _ heq
   use W', i₁ ≫ Opens.infLELeft U V, hxW'
-  -- Porting note : this `change` was not necessary in Lean3
-  change X.presheaf.map _ _ = X.presheaf.map _ _ at heq'
-  rw [map_one, map_mul] at heq'
-  -- Porting note : this `change` was not necessary in Lean3
-  change (X.presheaf.map _ ≫ X.presheaf.map _) _ * (X.presheaf.map _ ≫ _) _ = _ at heq'
-  rw [←X.presheaf.map_comp, ←op_comp] at heq'
+  rw [(X.presheaf.map i₂.op).map_one, (X.presheaf.map i₁.op).map_mul] at heq'
+  rw [← comp_apply, ←X.presheaf.map_comp, ←comp_apply, ←X.presheaf.map_comp, ←op_comp] at heq'
   exact isUnit_of_mul_eq_one _ _ heq'
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.RingedSpace.is_unit_res_of_is_unit_germ AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germ
@@ -130,13 +126,7 @@ theorem isUnit_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U))
   apply isUnit_of_mul_eq_one f gl
   apply X.sheaf.eq_of_locally_eq' V U iVU hcover
   intro i
-  -- Porting note : this `change` was not necessary in Lean3
-  change X.sheaf.1.map _ _ = X.sheaf.1.map _ 1
-  rw [RingHom.map_one, RingHom.map_mul]
-  -- Porting note : this `change` was not necessary in Lean3
-  specialize gl_spec i
-  change X.sheaf.1.map _ _ = _ at gl_spec
-  rw [gl_spec]
+  rw [RingHom.map_one, RingHom.map_mul, gl_spec]
   exact hg i
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.RingedSpace.is_unit_of_is_unit_germ AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germ
@@ -202,15 +192,11 @@ theorem basicOpen_res {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) (f : X.presheaf.obj
   let g := i.unop; have : i = g.op := rfl; clear_value g; subst this
   ext; constructor
   · rintro ⟨x, hx : IsUnit _, rfl⟩
-    -- Porting note : now need explicitly typing the rewrites and use `erw`
-    erw [show X.presheaf.germ x ((X.presheaf.map g.op) f) = X.presheaf.germ (g x) f
-     from X.presheaf.germ_res_apply _ _ _] at hx
+    erw [X.presheaf.germ_res_apply _ _ _] at hx
     exact ⟨x.2, g x, hx, rfl⟩
   · rintro ⟨hxV, x, hx, rfl⟩
     refine' ⟨⟨x, hxV⟩, (_ : IsUnit _), rfl⟩
-    -- Porting note : now need explicitly typing the rewrites and use `erw`
-    erw [show X.presheaf.germ ⟨x, hxV⟩ (X.presheaf.map g.op f) = X.presheaf.germ (g ⟨x, hxV⟩) f from
-      X.presheaf.germ_res_apply _ _ _]
+    erw [X.presheaf.germ_res_apply _ _ _]
     exact hx
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.RingedSpace.basic_open_res AlgebraicGeometry.RingedSpace.basicOpen_res
@@ -224,11 +210,9 @@ theorem basicOpen_res_eq {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) [IsIso i] (f : X.
     @basicOpen X (unop V) (X.presheaf.map i f) = @RingedSpace.basicOpen X (unop U) f := by
   apply le_antisymm
   · rw [X.basicOpen_res i f]; exact inf_le_right
-  · -- Porting note : now need explicitly typing the rewrites
-    have : X.basicOpen ((X.presheaf.map _ ≫ X.presheaf.map _) f) = _ :=
-      X.basicOpen_res (inv i) (X.presheaf.map i f)
-    rw [← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id] at this
-    erw [this]
+  · have := X.basicOpen_res (inv i) (X.presheaf.map i f)
+    rw [← comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id, id_apply] at this
+    rw [this]
     exact inf_le_right
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.RingedSpace.basic_open_res_eq AlgebraicGeometry.RingedSpace.basicOpen_res_eq

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -581,7 +581,7 @@ def stalkIso (x : PrimeSpectrum.Top R) :
       ext s
       simp only [FunctorToTypes.map_comp_apply, CommRingCat.forget_map,
         CommRingCat.coe_of, Category.comp_id]
-      rw [stalkToFiberRingHom_germ']
+      rw [comp_apply, comp_apply, stalkToFiberRingHom_germ']
       obtain ⟨V, hxV, iVU, f, g, (hg : V ≤ PrimeSpectrum.basicOpen _), hs⟩ :=
         exists_const _ _ s x hxU
       erw [← res_apply R U V iVU s ⟨x, hxV⟩, ← hs, const_apply, localizationToStalk_mk']

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -345,8 +345,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]
-        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)

Mathlib/AlgebraicTopology/TopologicalSimplex.lean

@@ -28,7 +28,7 @@ namespace SimplexCategory
 open Simplicial NNReal BigOperators Classical
 
 attribute [local instance]
-  CategoryTheory.ConcreteCategory.hasCoeToSort CategoryTheory.ConcreteCategory.hasCoeToFun
+  CategoryTheory.ConcreteCategory.hasCoeToSort CategoryTheory.ConcreteCategory.funLike
 
 -- porting note: added, should be moved
 instance (x : SimplexCategory) : Fintype (CategoryTheory.ConcreteCategory.forget.obj x) := by
@@ -98,14 +98,14 @@ def toTop : SimplexCategory ⥤ TopCat where
     apply toTopObj.ext
     funext i
     change (Finset.univ.filter fun k => k = i).sum _ = _
-    simp [Finset.sum_filter]
+    simp [Finset.sum_filter, CategoryTheory.id_apply]
   map_comp := fun f g => by
     ext h
     apply toTopObj.ext
     funext i
     dsimp
-    simp only [TopCat.comp_app]
-    simp only [TopCat.hom_apply, coe_toTopMap]
+    rw [CategoryTheory.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_mk, ContinuousMap.coe_mk]
+    simp only [coe_toTopMap]
     erw [← Finset.sum_biUnion]
     . apply Finset.sum_congr
       . exact Finset.ext (fun j => ⟨fun hj => by simpa using hj, fun hj => by simpa using hj⟩)