merge #7606

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

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

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₂

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -749,6 +749,9 @@ def subalgebraMap (e : A ≃ₐ[R] B) (S : Subalgebra R A) : S ≃ₐ[R] S.map e
       exact e.commutes _ }
 #align alg_equiv.subalgebra_map AlgEquiv.subalgebraMap
 
+-- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
+attribute [nolint simpNF] AlgEquiv.subalgebraMap_apply_coe AlgEquiv.subalgebraMap_symm_apply_coe
+
 end AlgEquiv
 
 namespace Algebra

Mathlib/Algebra/Category/AlgebraCat/Basic.lean

@@ -217,12 +217,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`

Mathlib/Algebra/Category/AlgebraCat/Limits.lean

@@ -104,17 +104,39 @@ def limitConeIsLimit (F : J ⥤ AlgebraCatMax.{v, w} R) : IsLimit (limitCone.{v,
   · -- Porting note: we could add a custom `ext` lemma here.
     apply Subtype.ext
     ext j
-    simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app]
+    simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app,
+      forget_map_eq_coe]
+    -- This used to be as below but we need `erw` after leanprover/lean4#2644
+    -- simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app]
+    erw [map_one]
     rfl
   · intro x y
     apply Subtype.ext
     ext j
-    simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app]
+    simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app,
+      forget_map_eq_coe]
+    -- This used to be as below, but we need `erw` after leanprover/lean4#2644
+    -- simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app]
+    erw [map_mul]
     rfl
-  · simp [forget_map_eq_coe, AlgHom.map_zero, Functor.mapCone_π_app]
+  · simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app,
+      forget_map_eq_coe]
+    -- The below `simp` was enough before leanprover/lean4#2644
+    -- simp [forget_map_eq_coe, AlgHom.map_zero, Functor.mapCone_π_app]
+    apply Subtype.ext
+    dsimp
+    funext u
+    erw [map_zero]
     rfl
   · intro x y
-    simp [forget_map_eq_coe, AlgHom.map_add, Functor.mapCone_π_app]
+    simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app,
+      forget_map_eq_coe]
+    -- The below `simp` was enough before leanprover/lean4#2644
+    -- simp [forget_map_eq_coe, AlgHom.map_add, Functor.mapCone_π_app]
+    apply Subtype.ext
+    dsimp
+    funext u
+    erw [map_add]
     rfl
   · intro r
     apply Subtype.ext

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.

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -154,6 +154,8 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddGroup.of_hom_apply AddGroupCat.ofHom_apply
 
+attribute [nolint simpNF] AddGroupCat.ofHom_apply GroupCat.ofHom_apply
+
 @[to_additive]
 instance ofUnique (G : Type*) [Group G] [i : Unique G] : Unique (GroupCat.of G) := i
 set_option linter.uppercaseLean3 false in
@@ -528,3 +530,4 @@ 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}
+

Mathlib/Algebra/Category/GroupCat/Biproducts.lean

@@ -76,6 +76,9 @@ noncomputable def biprodIsoProd (G H : AddCommGroupCat.{u}) :
   IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit G H) (binaryProductLimitCone G H).isLimit
 #align AddCommGroup.biprod_iso_prod AddCommGroupCat.biprodIsoProd
 
+-- simpNF now complains after leanprover/lean4#2644
+attribute [nolint simpNF] AddCommGroupCat.biprodIsoProd_hom_apply
+
 @[simp, elementwise]
 theorem biprodIsoProd_inv_comp_fst (G H : AddCommGroupCat.{u}) :
     (biprodIsoProd G H).inv ≫ biprod.fst = AddMonoidHom.fst G H :=
@@ -138,6 +141,9 @@ noncomputable def biproductIsoPi (f : J → AddCommGroupCat.{u}) :
   IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit
 #align AddCommGroup.biproduct_iso_pi AddCommGroupCat.biproductIsoPi
 
+-- simpNF now complains after leanprover/lean4#2644
+attribute [nolint simpNF] AddCommGroupCat.biproductIsoPi_hom_apply
+
 @[simp, elementwise]
 theorem biproductIsoPi_inv_comp_π (f : J → AddCommGroupCat.{u}) (j : J) :
     (biproductIsoPi f).inv ≫ biproduct.π f j = Pi.evalAddMonoidHom (fun j => f j) j :=

Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean

@@ -86,6 +86,12 @@ def groupAddGroupEquivalence : GroupCat ≌ AddGroupCat :=
     (NatIso.ofComponents fun X => AddEquiv.toAddGroupCatIso (AddEquiv.additiveMultiplicative X))
 #align Group_AddGroup_equivalence groupAddGroupEquivalence
 
+-- simpNF complains after leanprover/lean4#2466
+attribute [nolint simpNF] groupAddGroupEquivalence_unitIso_hom_app_apply
+  groupAddGroupEquivalence_counitIso_inv_app_apply
+  groupAddGroupEquivalence_unitIso_inv_app_apply
+  groupAddGroupEquivalence_counitIso_hom_app_apply
+
 /-- The equivalence of categories between `CommGroup` and `AddCommGroup`.
 -/
 @[simps!]
@@ -94,3 +100,9 @@ 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
+
+-- simpNF complains after leanprover/lean4#2466
+attribute [nolint simpNF] commGroupAddCommGroupEquivalence_counitIso_hom_app_apply
+  commGroupAddCommGroupEquivalence_unitIso_inv_app_apply
+  commGroupAddCommGroupEquivalence_unitIso_hom_app_apply
+  commGroupAddCommGroupEquivalence_counitIso_inv_app_apply

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

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -465,4 +465,8 @@ def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.kernel_iso_ker_over AddCommGroupCat.kernelIsoKerOver
 
+-- simpNF complains after leanprover/lean4#2466
+attribute [nolint simpNF] AddCommGroupCat.kernelIsoKerOver_inv_left_apply
+  AddCommGroupCat.kernelIsoKerOver_hom_left_apply_coe
+
 end AddCommGroupCat

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -75,7 +75,7 @@ def ε : 𝟙_ (ModuleCat.{u} R) ⟶ (free R).obj (𝟙_ (Type u)) :=
   Finsupp.lsingle PUnit.unit
 #align Module.free.ε ModuleCat.Free.ε
 
-@[simp]
+@[simp, nolint simpNF]
 theorem ε_apply (r : R) : ε R r = Finsupp.single PUnit.unit r :=
   rfl
 #align Module.free.ε_apply ModuleCat.Free.ε_apply
@@ -103,8 +103,10 @@ theorem μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') :
     (Finsupp.mapDomain f (Finsupp.single x 1) ⊗ₜ[R] Finsupp.mapDomain g (Finsupp.single x' 1)) _
     = (Finsupp.mapDomain (f ⊗ g) (finsuppTensorFinsupp' R X X'
     (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single x' 1))) _
+
+  -- extra `rfl` after leanprover/lean4#2466
   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) :
@@ -175,8 +177,9 @@ theorem associativity (X Y Z : Type u) :
     finsuppTensorFinsupp' R X (Y ⊗ Z)
     (Finsupp.single x 1 ⊗ₜ[R]
       finsuppTensorFinsupp' R Y Z (Finsupp.single y 1 ⊗ₜ[R] Finsupp.single z 1)) a
+  -- extra `rfl` after leanprover/lean4#2466
   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 +425,4 @@ 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
-
 end CategoryTheory

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

Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

@@ -77,6 +77,9 @@ noncomputable def biprodIsoProd (M N : ModuleCat.{v} R) :
   IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit M N) (binaryProductLimitCone M N).isLimit
 #align Module.biprod_iso_prod ModuleCat.biprodIsoProd
 
+-- simpNF complains after leanprover/lean4#2644
+attribute [nolint simpNF] ModuleCat.biprodIsoProd_hom_apply
+
 @[simp, elementwise]
 theorem biprodIsoProd_inv_comp_fst (M N : ModuleCat.{v} R) :
     (biprodIsoProd M N).inv ≫ biprod.fst = LinearMap.fst R M N :=
@@ -138,6 +141,9 @@ noncomputable def biproductIsoPi [Fintype J] (f : J → ModuleCat.{v} R) :
   IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit
 #align Module.biproduct_iso_pi ModuleCat.biproductIsoPi
 
+-- simpNF complains after leanprover/lean4#2644
+attribute [nolint simpNF] ModuleCat.biproductIsoPi_hom_apply
+
 @[simp, elementwise]
 theorem biproductIsoPi_inv_comp_π [Fintype J] (f : J → ModuleCat.{v} R) (j : J) :
     (biproductIsoPi f).inv ≫ biproduct.π f j = (LinearMap.proj j : (∀ j, f j) →ₗ[R] f j) :=

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -743,8 +743,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]
+      rw [lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
       set s' : S := s'
       change s' • g y = g (s' • y)
       rw [map_smul]
@@ -772,8 +774,12 @@ 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,
-          ExtendRestrictScalarsAdj.counit_app, ExtendRestrictScalarsAdj.Counit.map_apply]
+      · rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply]
+        -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+        erw [ModuleCat.coe_comp]
+        rw [Function.comp_apply, ExtendRestrictScalarsAdj.counit_app]
+        -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+        erw [ExtendRestrictScalarsAdj.Counit.map_apply]
         dsimp
         rw [TensorProduct.lift.tmul]
         rfl
@@ -788,5 +794,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

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]

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -39,8 +39,9 @@ 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,
-            HasZeroMorphisms.comp_zero (Fork.ι s) N]
+          -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+          erw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← coe_comp]
+          rw [Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N]
           rfl)
     (fun s => LinearMap.subtype_comp_codRestrict _ _ _) fun s m h =>
     LinearMap.ext fun x => Subtype.ext_iff_val.2 (by simp [← h]; rfl)

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -277,23 +277,31 @@ 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,
-      TensorProduct.tmul_zero]
+    rw [LinearMap.zero_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [MonoidalCategory.hom_apply]
+    rw [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,
-      TensorProduct.zero_tmul]
+    rw [LinearMap.zero_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [MonoidalCategory.hom_apply]
+    rw [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]
+    rw [LinearMap.add_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [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]
+    rw [LinearMap.add_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
     erw [MonoidalCategory.hom_apply]
     rw [LinearMap.add_apply, TensorProduct.add_tmul]
 
@@ -303,12 +311,16 @@ 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,
-      LinearMap.smul_apply, TensorProduct.tmul_smul]
+    rw [LinearMap.smul_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    rw [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,
-      LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul]
+    rw [LinearMap.smul_apply]
+    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
+    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    rw [LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul]
 
 end ModuleCat