chore: revert #7703 (#7710)

This reverts commit 26eb2b0.

Archive/Sensitivity.lean

@@ -216,7 +216,6 @@ 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,8 +88,7 @@ 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
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [DFinsupp.zero_apply, DFinsupp.add_apply, DFinsupp.single_eq_same,
+    rw [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,15 +87,13 @@ theorem x_not_pseudo_eq : ¬PseudoEqual _ x y := by
     Preadditive.comp_add] at ha
   let π₁ := (biprod.fst : of ℤ ℚ ⊞ of ℤ ℚ ⟶ _)
   have ha₁ := congr_arg π₁ ha
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₁
+  rw [← 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
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [← CategoryTheory.comp_apply, ← CategoryTheory.comp_apply] at ha₂
+  rw [← 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,9 +749,6 @@ 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,14 +217,12 @@ 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]
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [id_apply]
+    rw [id_apply]
   right_inv x := by
     -- porting note: was `by tidy`
     change (i.inv ≫ i.hom) x = x
     simp only [inv_hom_id]
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [id_apply]
+    rw [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,39 +104,17 @@ 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 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]
+    simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app]
     rfl
   · intro x y
     apply Subtype.ext
     ext j
-    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]
+    simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app]
     rfl
-  · 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]
+  · simp [forget_map_eq_coe, AlgHom.map_zero, Functor.mapCone_π_app]
     rfl
   · intro x y
-    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]
+    simp [forget_map_eq_coe, AlgHom.map_add, Functor.mapCone_π_app]
     rfl
   · intro r
     apply Subtype.ext

Mathlib/Algebra/Category/GroupCat/Adjunctions.lean

@@ -60,9 +60,7 @@ theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = FreeAbelianGroup 
   rfl
 #align AddCommGroup.free_obj_coe AddCommGroupCat.free_obj_coe
 
--- This currently can't be a `simp` lemma,
--- because `free_obj_coe` will simplify implicit arguments in the LHS.
--- (The `simpNF` linter will, correctly, complain.)
+@[simp]
 theorem free_map_coe {α β : Type u} {f : α → β} (x : FreeAbelianGroup α) :
     (free.map f) x = f <$> x :=
   rfl
@@ -104,11 +102,9 @@ def free : Type u ⥤ GroupCat where
   obj α := of (FreeGroup α)
   map := FreeGroup.map
   map_id := by
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    intros; ext1; erw [←FreeGroup.map.unique] <;> intros <;> rfl
+    intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl
   map_comp := by
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    intros; ext1; erw [←FreeGroup.map.unique] <;> intros <;> rfl
+    intros; ext1; rw [←FreeGroup.map.unique]; intros; rfl
 #align Group.free GroupCat.free
 
 /-- The free-forgetful adjunction for groups.

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -154,9 +154,6 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddGroup.of_hom_apply AddGroupCat.ofHom_apply
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-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

Mathlib/Algebra/Category/GroupCat/Biproducts.lean

@@ -76,9 +76,6 @@ noncomputable def biprodIsoProd (G H : AddCommGroupCat.{u}) :
   IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit G H) (binaryProductLimitCone G H).isLimit
 #align AddCommGroup.biprod_iso_prod AddCommGroupCat.biprodIsoProd
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-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 :=
@@ -141,9 +138,6 @@ noncomputable def biproductIsoPi (f : J → AddCommGroupCat.{u}) :
   IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit
 #align AddCommGroup.biproduct_iso_pi AddCommGroupCat.biproductIsoPi
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-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,12 +86,6 @@ def groupAddGroupEquivalence : GroupCat ≌ AddGroupCat :=
     (NatIso.ofComponents fun X => AddEquiv.toAddGroupCatIso (AddEquiv.additiveMultiplicative X))
 #align Group_AddGroup_equivalence groupAddGroupEquivalence
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-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!]
@@ -100,9 +94,3 @@ 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
-
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-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,8 +133,7 @@ variable {a}
 
 lemma eq_zero_of_toRatCircle_apply_self
     (h : toRatCircle ⟨a, Submodule.mem_span_singleton_self a⟩ = 0) : a = 0 := by
-  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-  erw [toRatCircle, LinearMap.comp_apply, LinearEquiv.coe_toLinearMap,
+  rw [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,8 +465,4 @@ def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.kernel_iso_ker_over AddCommGroupCat.kernelIsoKerOver
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-attribute [nolint simpNF] AddCommGroupCat.kernelIsoKerOver_inv_left_apply
-  AddCommGroupCat.kernelIsoKerOver_hom_left_apply_coe
-
 end AddCommGroupCat

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -75,8 +75,7 @@ def ε : 𝟙_ (ModuleCat.{u} R) ⟶ (free R).obj (𝟙_ (Type u)) :=
   Finsupp.lsingle PUnit.unit
 #align Module.free.ε ModuleCat.Free.ε
 
--- This lemma has always been bad, but lean4#2644 made `simp` start noticing
-@[simp, nolint simpNF]
+@[simp]
 theorem ε_apply (r : R) : ε R r = Finsupp.single PUnit.unit r :=
   rfl
 #align Module.free.ε_apply ModuleCat.Free.ε_apply
@@ -104,10 +103,8 @@ 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]; rfl
+    Finsupp.mapDomain_single, CategoryTheory.tensor_apply]
 #align Module.free.μ_natural ModuleCat.Free.μ_natural
 
 theorem left_unitality (X : Type u) :
@@ -178,9 +175,8 @@ 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]; rfl
+    CategoryTheory.associator_hom_apply]
 #align Module.free.associativity ModuleCat.Free.associativity
 
 -- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
@@ -426,4 +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
+
 end CategoryTheory

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -445,8 +445,7 @@ instance : Module R (mkOfSMul' φ) where
 given by `R`. -/
 abbrev mkOfSMul := ModuleCat.of R (mkOfSMul' φ)
 
--- This lemma has always been bad, but lean4#2644 made `simp` start noticing
-@[simp, nolint simpNF]
+@[simp]
 lemma mkOfSMul_smul (r : R) : (mkOfSMul φ).smul r = φ r := rfl
 
 end

Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

@@ -77,9 +77,6 @@ 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
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-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 :=
@@ -141,9 +138,6 @@ 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
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-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

@@ -156,13 +156,11 @@ variable {R : Type u₁} [Ring R] (f : R →+* R) (hf : f = RingHom.id R)
 identity functor. -/
 def restrictScalarsId' : ModuleCat.restrictScalars.{v} f ≅ 𝟭 _ := by subst hf; rfl
 
--- This lemma has always been bad, but lean4#2644 made `simp` start noticing
-@[simp, nolint simpNF]
+@[simp]
 lemma restrictScalarsId'_inv_apply (M : ModuleCat R) (x : M) :
     (restrictScalarsId' f hf).inv.app M x = x := by subst hf; rfl
 
--- This lemma has always been bad, but lean4#2644 made `simp` start noticing
-@[simp, nolint simpNF]
+@[simp]
 lemma restrictScalarsId'_hom_apply (M : ModuleCat R) (x : M) :
     (restrictScalarsId' f hf).hom.app M x = x := by subst hf; rfl
 
@@ -184,14 +182,11 @@ composition of the restriction of scalars functors. -/
 def restrictScalarsComp' :
     ModuleCat.restrictScalars.{v} gf ≅
       ModuleCat.restrictScalars g ⋙ ModuleCat.restrictScalars f := by subst hgf; rfl
-
--- This lemma has always been bad, but lean4#2644 made `simp` start noticing
-@[simp, nolint simpNF]
+@[simp]
 lemma restrictScalarsComp'_hom_apply (M : ModuleCat R₃) (x : M) :
     (restrictScalarsComp' f g gf hgf).hom.app M x = x := by subst hgf; rfl
 
--- This lemma has always been bad, but lean4#2644 made `simp` start noticing
-@[simp, nolint simpNF]
+@[simp]
 lemma restrictScalarsComp'_inv_apply (M : ModuleCat R₃) (x : M) :
     (restrictScalarsComp' f g gf hgf).inv.app M x = x := by subst hgf; rfl
 
@@ -748,10 +743,8 @@ 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]
-      -- 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]
+        ExtendScalars.map_tmul, restrictScalars.map_apply, Counit.map_apply, Counit.map_apply,
+        lift.tmul, lift.tmul, LinearMap.coe_mk, LinearMap.coe_mk]
       set s' : S := s'
       change s' • g y = g (s' • y)
       rw [map_smul]
@@ -779,12 +772,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]
-        -- 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]
+      · rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply, ModuleCat.coe_comp, Function.comp_apply,
+          ExtendRestrictScalarsAdj.counit_app, ExtendRestrictScalarsAdj.Counit.map_apply]
         dsimp
         rw [TensorProduct.lift.tmul]
         rfl

Mathlib/Algebra/Category/ModuleCat/Colimits.lean

@@ -61,8 +61,7 @@ noncomputable def colimitCocone : Cocone F where
   ι :=
     { app := fun j => homMk (colimit.ι (F ⋙ forget₂ _ AddCommGroupCat)  j) (fun r => by
         dsimp
-        -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-        erw [mkOfSMul_smul]
+        rw [mkOfSMul_smul]
         simp)
       naturality := fun i j f => by
         apply (forget₂ _ AddCommGroupCat).map_injective
@@ -78,8 +77,7 @@ noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F) where
     intro j
     dsimp
     rw [colimit.ι_desc_assoc]
-    -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [mkOfSMul_smul]
+    rw [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,9 +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
-          -- 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]
+          rw [← @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 =>
     LinearMap.ext fun x => Subtype.ext_iff_val.2 (by simp [← h]; rfl)