leanprover-community · semorrison · Sep 19, 2023 · Sep 19, 2023 · Sep 19, 2023 · Sep 19, 2023
diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean
@@ -216,6 +216,7 @@ theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
   · rw [show p = q from Subsingleton.elim (α := Q 0) p q]
     dsimp [ε, e]
     simp
+    rfl
   · dsimp [ε, e]
     cases hp : p 0 <;> cases hq : q 0
     all_goals

diff --git a/Counterexamples/DirectSumIsInternal.lean b/Counterexamples/DirectSumIsInternal.lean
@@ -88,7 +88,8 @@ theorem withSign.not_injective :
     -- porting note: `DFinsupp.singleAddHom_apply` doesn't work so we have to unfold
     dsimp [DirectSum.lof_eq_of, DirectSum.of, DFinsupp.singleAddHom] at h
     replace h := FunLike.congr_fun h 1
-    rw [DFinsupp.zero_apply, DFinsupp.add_apply, DFinsupp.single_eq_same,
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [DFinsupp.zero_apply, DFinsupp.add_apply, DFinsupp.single_eq_same,
       DFinsupp.single_eq_of_ne UnitsInt.one_ne_neg_one.symm, add_zero, Subtype.ext_iff,
       Submodule.coe_zero] at h
     apply zero_ne_one h.symm

diff --git a/Counterexamples/Pseudoelement.lean b/Counterexamples/Pseudoelement.lean
@@ -87,13 +87,15 @@ theorem x_not_pseudo_eq : ¬PseudoEqual _ x y := by
     Preadditive.comp_add] at ha
   let π₁ := (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _)
   have ha₁ := congr_arg π₁ ha
-  rw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₁
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644  
+  erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₁
   simp only [BinaryBiproduct.bicone_fst, biprod.lift_fst, CategoryTheory.id_apply,
     biprod.lift_fst_assoc, Category.id_comp, biprod.lift_snd_assoc, Linear.smul_comp,
     Preadditive.add_comp, BinaryBicone.inl_fst, BinaryBicone.inr_fst, smul_zero, add_zero] at ha₁
   let π₂ := (biprod.snd : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _)
   have ha₂ := congr_arg π₂ ha
-  rw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₂
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+  erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₂
   simp only [BinaryBiproduct.bicone_snd, biprod.lift_snd, CategoryTheory.id_apply,
     biprod.lift_fst_assoc, Category.id_comp, biprod.lift_snd_assoc, Linear.smul_comp,
     Preadditive.add_comp, BinaryBicone.inl_snd, BinaryBicone.inr_snd, zero_add, two_smul] at ha₂

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@@ -741,7 +741,7 @@ noncomputable def ofInjectiveField {E F : Type*} [DivisionRing E] [Semiring F] [
 
 /-- Given an equivalence `e : A ≃ₐ[R] B` of `R`-algebras and a subalgebra `S` of `A`,
 `subalgebra_map` is the induced equivalence between `S` and `S.map e` -/
-@[simps!]
+@[simps!, nolint simpNF]
 def subalgebraMap (e : A ≃ₐ[R] B) (S : Subalgebra R A) : S ≃ₐ[R] S.map e.toAlgHom :=
   { e.toRingEquiv.subsemiringMap S.toSubsemiring with
     commutes' := fun r => by
@@ -1509,4 +1509,5 @@ theorem mem_subalgebraOfSubring {x : R} {S : Subring R} : x ∈ subalgebraOfSubr
   Iff.rfl
 #align mem_subalgebra_of_subring mem_subalgebraOfSubring
 
+attribute [nolint simpNF] AlgEquiv.subalgebraMap_apply_coe AlgEquiv.subalgebraMap_symm_apply_coe
 end Int
diff --git a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean
@@ -207,12 +207,14 @@ def toAlgEquiv {X Y : AlgebraCat R} (i : X ≅ Y) : X ≃ₐ[R] Y where
     -- porting note: was `by tidy`
     change (i.hom ≫ i.inv) x = x
     simp only [hom_inv_id]
-    rw [id_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [id_apply]
   right_inv x := by
     -- porting note: was `by tidy`
     change (i.inv ≫ i.hom) x = x
     simp only [inv_hom_id]
-    rw [id_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [id_apply]
   map_add' := i.hom.map_add -- Porting note: was `by tidy`
   map_mul' := i.hom.map_mul -- Porting note: was `by tidy`
   commutes' := i.hom.commutes -- Porting note: was `by tidy`

diff --git a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean
@@ -105,16 +105,30 @@ def limitConeIsLimit (F : J ⥤ AlgebraCatMax.{v, w} R) : IsLimit (limitCone.{v,
     apply Subtype.ext
     ext j
     simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [map_one]
     rfl
   · intro x y
     apply Subtype.ext
     ext j
     simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [map_mul]
     rfl
   · simp [forget_map_eq_coe, AlgHom.map_zero, Functor.mapCone_π_app]
+    -- The above `simp` was enough before leanprover/lean4#2644
+    apply Subtype.ext
+    dsimp
+    funext u
+    erw [map_zero]
     rfl
   · intro x y
     simp [forget_map_eq_coe, AlgHom.map_add, Functor.mapCone_π_app]
+    -- The above `simp` was enough before leanprover/lean4#2644
+    apply Subtype.ext
+    dsimp
+    funext u
+    erw [map_add]
     rfl
   · intro r
     apply Subtype.ext

diff --git a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean
@@ -60,7 +60,7 @@ theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = FreeAbelianGroup
   rfl
 #align AddCommGroup.free_obj_coe AddCommGroupCat.free_obj_coe
 
-@[simp]
+@[simp, nolint simpNF]
 theorem free_map_coe {α β : Type u} {f : α → β} (x : FreeAbelianGroup α) :
     (free.map f) x = f <$> x :=
   rfl
@@ -102,9 +102,11 @@ def free : Type u ⥤ GroupCat where
   obj α := of (FreeGroup α)
   map := FreeGroup.map
   map_id := by
-    intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    intros; ext1; erw [←FreeGroup.map.unique] <;> intros <;> rfl
   map_comp := by
-    intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    intros; ext1; erw [←FreeGroup.map.unique] <;> intros <;> rfl
 #align Group.free GroupCat.free
 
 /-- The free-forgetful adjunction for groups.

diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean
@@ -134,7 +134,7 @@ set_option linter.uppercaseLean3 false in
 #align AddGroup.zero_apply AddGroupCat.zero_apply
 
 /-- Typecheck a `MonoidHom` as a morphism in `GroupCat`. -/
-@[to_additive]
+@[to_additive, nolint simpNF]
 def ofHom {X Y : Type u} [Group X] [Group Y] (f : X →* Y) : of X ⟶ of Y :=
   f
 set_option linter.uppercaseLean3 false in
@@ -528,3 +528,5 @@ abbrev CommGroupCatMax.{u1, u2} := CommGroupCat.{max u1 u2}
 /-- An alias for `AddCommGroupCat.{max u v}`, to deal around unification issues. -/
 @[nolint checkUnivs]
 abbrev AddCommGroupCatMax.{u1, u2} := AddCommGroupCat.{max u1 u2}
+
+attribute [nolint simpNF] AddGroupCat.ofHom_apply GroupCat.ofHom_apply
diff --git a/Mathlib/Algebra/Category/GroupCat/Biproducts.lean b/Mathlib/Algebra/Category/GroupCat/Biproducts.lean
@@ -144,4 +144,6 @@ theorem biproductIsoPi_inv_comp_π (f : J → AddCommGroupCat.{u}) (j : J) :
   IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk j)
 #align AddCommGroup.biproduct_iso_pi_inv_comp_π AddCommGroupCat.biproductIsoPi_inv_comp_π
 
+attribute [nolint simpNF] AddCommGroupCat.biprodIsoProd_hom_apply
+  AddCommGroupCat.biproductIsoPi_hom_apply
 end AddCommGroupCat
diff --git a/Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean b/Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean
@@ -94,3 +94,12 @@ def commGroupAddCommGroupEquivalence : CommGroupCat ≌ AddCommGroupCat :=
     (NatIso.ofComponents fun X => MulEquiv.toCommGroupCatIso (MulEquiv.multiplicativeAdditive X))
     (NatIso.ofComponents fun X => AddEquiv.toAddCommGroupCatIso (AddEquiv.additiveMultiplicative X))
 #align CommGroup_AddCommGroup_equivalence commGroupAddCommGroupEquivalence
+
+attribute [nolint simpNF] groupAddGroupEquivalence_unitIso_hom_app_apply
+  groupAddGroupEquivalence_counitIso_inv_app_apply
+  groupAddGroupEquivalence_unitIso_inv_app_apply
+  groupAddGroupEquivalence_counitIso_hom_app_apply
+  commGroupAddCommGroupEquivalence_counitIso_hom_app_apply
+  commGroupAddCommGroupEquivalence_unitIso_inv_app_apply
+  commGroupAddCommGroupEquivalence_unitIso_hom_app_apply
+  commGroupAddCommGroupEquivalence_counitIso_inv_app_apply
diff --git a/Mathlib/Algebra/Category/GroupCat/Injective.lean b/Mathlib/Algebra/Category/GroupCat/Injective.lean
@@ -133,7 +133,8 @@ variable {a}
 
 lemma eq_zero_of_toRatCircle_apply_self
     (h : toRatCircle ⟨a, Submodule.mem_span_singleton_self a⟩ = 0) : a = 0 := by
-  rw [toRatCircle, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap,
+  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+  erw [toRatCircle, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap,
     equivZModSpanAddOrderOf_apply_self, Submodule.liftQSpanSingleton_apply,
     LinearMap.toSpanSingleton_one, AddCircle.coe_eq_zero_iff] at h
   obtain ⟨n, hn⟩ := h

diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean
@@ -464,5 +464,6 @@ def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
   Over.isoMk (kernelIsoKer f)
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.kernel_iso_ker_over AddCommGroupCat.kernelIsoKerOver
-
+attribute [nolint simpNF] AddCommGroupCat.kernelIsoKerOver_inv_left_apply
+  AddCommGroupCat.kernelIsoKerOver_hom_left_apply_coe
 end AddCommGroupCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@@ -104,7 +104,7 @@ theorem μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') :
     = (Finsupp.mapDomain (f ⊗ g) (finsuppTensorFinsupp' R X X'
     (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single x' 1))) _
   simp_rw [Finsupp.mapDomain_single, finsuppTensorFinsupp'_single_tmul_single, mul_one,
-    Finsupp.mapDomain_single, CategoryTheory.tensor_apply]
+    Finsupp.mapDomain_single, CategoryTheory.tensor_apply]; rfl
 #align Module.free.μ_natural ModuleCat.Free.μ_natural
 
 theorem left_unitality (X : Type u) :
@@ -176,7 +176,7 @@ theorem associativity (X Y Z : Type u) :
     (Finsupp.single x 1 ⊗ₜ[R]
       finsuppTensorFinsupp' R Y Z (Finsupp.single y 1 ⊗ₜ[R] Finsupp.single z 1)) a
   simp_rw [finsuppTensorFinsupp'_single_tmul_single, Finsupp.mapDomain_single, mul_one,
-    CategoryTheory.associator_hom_apply]
+    CategoryTheory.associator_hom_apply]; rfl
 #align Module.free.associativity ModuleCat.Free.associativity
 
 -- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
@@ -422,5 +422,5 @@ def liftUnique (F : C ⥤ D) (L : Free R C ⥤ D) [L.Additive] [L.Linear R]
 #align category_theory.Free.lift_unique CategoryTheory.Free.liftUnique
 
 end Free
-
+attribute [nolint simpNF] ModuleCat.Free.ε_apply
 end CategoryTheory
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -470,5 +470,5 @@ lemma forget₂_map_homMk :
     (forget₂ (ModuleCat R) AddCommGroupCat).map (homMk φ hφ) = φ := rfl
 
 end
-
+attribute [nolint simpNF] ModuleCat.mkOfSMul_smul
 end ModuleCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean b/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean
@@ -175,4 +175,5 @@ noncomputable def lequivProdOfLeftSplitExact {f : M →ₗ[R] A} (hg : Function.
     biprodIsoProd _ _).toLinearEquiv.symm
 #align lequiv_prod_of_left_split_exact lequivProdOfLeftSplitExact
 
+attribute [nolint simpNF] ModuleCat.biprodIsoProd_hom_apply ModuleCat.biproductIsoPi_hom_apply
 end SplitExact
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -207,6 +207,7 @@ variable (M : Type v) [AddCommMonoid M] [Module R M]
 -- mathport name: «expr ⊗ₜ[ , ] »
 -- This notation is necessary because we need to reason about `s ⊗ₜ m` where `s : S` and `m : M`;
 -- without this notation, one need to work with `s : (restrictScalars f).obj ⟨S⟩`.
+/-- Tensor multiplication using a ring morphism. -/
 scoped[ChangeOfRings]
   notation s "⊗ₜ[" R "," f "]" m => @TensorProduct.tmul R _ _ _ _ _ (Module.compHom _ f) _ s m
 
@@ -743,8 +744,10 @@ def counit : restrictScalars.{max v u₂,u₁,u₂} f ⋙ extendScalars f ⟶
     · rw [map_zero, map_zero]
     · dsimp
       rw [ModuleCat.coe_comp, ModuleCat.coe_comp,Function.comp,Function.comp,
-        ExtendScalars.map_tmul, restrictScalars.map_apply, Counit.map_apply, Counit.map_apply,
-        lift.tmul, lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
+        ExtendScalars.map_tmul, restrictScalars.map_apply]
+      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+      erw [Counit.map_apply] --Counit.map_apply,
+      rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
       set s' : S := s'
       change s' • g y = g (s' • y)
       rw [map_smul]
@@ -772,7 +775,8 @@ def extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommR
       letI m2 : Module R Y := Module.compHom Y f
       induction' x using TensorProduct.induction_on with s x _ _ _ _
       · rw [map_zero, map_zero]
-      · rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply, ModuleCat.coe_comp, Function.comp_apply,
+      · -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+        erw [ExtendRestrictScalarsAdj.homEquiv_symm_apply, ModuleCat.coe_comp, Function.comp_apply,
           ExtendRestrictScalarsAdj.counit_app, ExtendRestrictScalarsAdj.Counit.map_apply]
         dsimp
         rw [TensorProduct.lift.tmul]
@@ -788,5 +792,6 @@ instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+*
 instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
     CategoryTheory.IsRightAdjoint (restrictScalars f) :=
   ⟨_, extendRestrictScalarsAdj f⟩
-
+attribute [nolint simpNF] restrictScalarsId'_inv_apply  restrictScalarsId'_hom_apply
+  restrictScalarsComp'_hom_apply restrictScalarsComp'_inv_apply
 end ModuleCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean
@@ -61,7 +61,8 @@ noncomputable def colimitCocone : Cocone F where
   ι :=
     { app := fun j => homMk (colimit.ι (F ⋙ forget₂ _ AddCommGroupCat)  j) (fun r => by
         dsimp
-        rw [mkOfSMul_smul]
+        -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+        erw [mkOfSMul_smul]
         simp)
       naturality := fun i j f => by
         apply (forget₂ _ AddCommGroupCat).map_injective
@@ -77,7 +78,8 @@ noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F) where
     intro j
     dsimp
     rw [colimit.ι_desc_assoc]
-    rw [mkOfSMul_smul]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [mkOfSMul_smul]
     dsimp
     simp only [ι_colimMap_assoc, Functor.comp_obj, forget₂_obj, colimit.ι_desc,
       Functor.mapCocone_pt, Functor.mapCocone_ι_app, forget₂_map]

diff --git a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean
@@ -39,7 +39,8 @@ def kernelIsLimit : IsLimit (kernelCone f) :=
     -- Porting note: broken dot notation on LinearMap.ker
       LinearMap.codRestrict (LinearMap.ker f) (Fork.ι s) fun c =>
         LinearMap.mem_ker.2 <| by
-          rw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← coe_comp, Fork.condition,
+          -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+          erw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← coe_comp, Fork.condition,
             HasZeroMorphisms.comp_zero (Fork.ι s) N]
           rfl)
     (fun s => LinearMap.subtype_comp_codRestrict _ _ _) fun s m h =>

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -277,23 +277,27 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
-    rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply,
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply,
       TensorProduct.tmul_zero]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
-    rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply,
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply,
       TensorProduct.zero_tmul]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
-    rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
     erw [MonoidalCategory.hom_apply]
     rw [LinearMap.add_apply, TensorProduct.tmul_add]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
-    rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
     erw [MonoidalCategory.hom_apply]
     rw [LinearMap.add_apply, TensorProduct.add_tmul]
 
@@ -303,12 +307,14 @@ instance : MonoidalLinear R (ModuleCat.{u} R) := by
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
-    rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply,
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply,
       LinearMap.smul_apply, TensorProduct.tmul_smul]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
-    rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply,
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply,
       LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul]
 
 end ModuleCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
@@ -34,7 +34,8 @@ def monoidalClosedHomEquiv (M N P : ModuleCat.{u} R) :
   left_inv f := by
     apply TensorProduct.ext'
     intro m n
-    rw [coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply,
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply,
       TensorProduct.lift.tmul, LinearMap.compr₂_apply,
       TensorProduct.mk_apply, coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply]
   right_inv f := rfl
@@ -106,4 +107,5 @@ theorem monoidalClosed_pre_app {M N : ModuleCat.{u} R} (P : ModuleCat.{u} R) (f
 set_option linter.uppercaseLean3 false in
 #align Module.monoidal_closed_pre_app ModuleCat.monoidalClosed_pre_app
 
+attribute [nolint simpNF] ModuleCat.monoidalClosed_curry
 end ModuleCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Projective.lean b/Mathlib/Algebra/Category/ModuleCat/Projective.lean
@@ -69,7 +69,8 @@ instance moduleCat_enoughProjectives : EnoughProjectives (ModuleCat.{max u v} R)
               -- Porting note: simp [Finsupp.total_single] fails but rw succeeds
               dsimp [Basis.constr]
               simp only [Finsupp.lmapDomain_id, comp_id]
-              rw [Finsupp.total_single, one_smul]
+              -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+              erw [Finsupp.total_single, one_smul]
               rfl ⟩) }⟩
 set_option linter.uppercaseLean3 false in
 #align Module.Module_enough_projectives ModuleCat.moduleCat_enoughProjectives

diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean
@@ -403,7 +403,8 @@ add_decl_doc addEquivIsoAddCommMonCatIso
 instance MonCat.forget_reflects_isos : ReflectsIsomorphisms (forget MonCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget MonCat).map f)
-    let e : X ≃* Y := MulEquiv.mk i.toEquiv (by aesop)
+    -- Again a problem that exists already creeps into other things
+    let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f))
     exact IsIso.of_iso e.toMonCatIso
 set_option linter.uppercaseLean3 false in
 #align Mon.forget_reflects_isos MonCat.forget_reflects_isos

diff --git a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean
@@ -312,7 +312,8 @@ def colimitDesc (t : Cocone F) : colimit.{v, u} F ⟶ t.pt where
     rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j)
       (IsFiltered.rightToMax i j)]
     dsimp [Types.colimitCoconeIsColimit]
-    rw [MonoidHom.map_mul]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [MonoidHom.map_mul]
     -- Porting note : `rw` can't see through coercion is actually forgetful functor,
     -- so can't rewrite `t.w_apply`
     congr 1 <;>