chore(Algebra/Category): clean up erw and porting notes (#22249)

I searched for `erw` and `porting note` and did my best to fix them. We still have lots of ugly `erw`s in (presheaves of) `ModuleCat`, unfortunately...




Co-authored-by: Anne Baanen <[email protected]>

Mathlib/Algebra/Algebra/Defs.lean

@@ -191,6 +191,11 @@ theorem RingHom.algebraMap_toAlgebra' {R S} [CommSemiring R] [Semiring S] (i : R
 def RingHom.toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) : Algebra R S :=
   i.toAlgebra' fun _ => mul_comm _
 
+theorem RingHom.smul_toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S)
+    (r : R) (s : S) :
+    let _ := RingHom.toAlgebra i
+    r • s = i r * s := rfl
+
 theorem RingHom.algebraMap_toAlgebra {R S} [CommSemiring R] [CommSemiring S] (i : R →+* S) :
     @algebraMap R S _ _ i.toAlgebra = i :=
   rfl

Mathlib/Algebra/Category/AlgebraCat/Limits.lean

@@ -135,8 +135,6 @@ end HasLimits
 
 open HasLimits
 
--- Porting note: mathport translated this as `irreducible_def`, but as `HasLimitsOfSize`
--- is a `Prop`, declaring this as `irreducible` should presumably have no effect
 /-- The category of R-algebras has all limits. -/
 lemma hasLimitsOfSize [UnivLE.{v, w}] : HasLimitsOfSize.{t, v} (AlgebraCat.{w} R) :=
   { has_limits_of_shape := fun _ _ =>

Mathlib/Algebra/Category/BoolRing.lean

@@ -96,11 +96,12 @@ end BoolRing
 
 /-! ### Equivalence between `BoolAlg` and `BoolRing` -/
 
--- Porting note: Added. somehow it does not find this instance.
+-- We have to add this instance since Lean doesn't see through `X.toBddDistLat`.
 instance {X : BoolAlg} :
     BooleanAlgebra ↑(BddDistLat.toBddLat (X.toBddDistLat)).toLat :=
   BoolAlg.str _
 
+-- We have to add this instance since Lean doesn't see through `R.toBddDistLat`.
 instance {R : Type u} [BooleanRing R] :
     BooleanRing (BoolAlg.of (AsBoolAlg ↑R)).toBddDistLat.toBddLat.toLat :=
   inferInstanceAs <| BooleanRing R

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -204,9 +204,7 @@ instance closedPredicateModuleFinite :
 
 instance : MonoidalClosed (FGModuleCat K) := by
   dsimp [FGModuleCat]
-  -- Porting note (https://github.com/leanprover-community/mathlib4/pull/11187): was `infer_instance`
-  exact MonoidalCategory.fullMonoidalClosedSubcategory
-    (fun V : ModuleCat.{u} K => Module.Finite K V)
+  infer_instance
 
 variable (V W : FGModuleCat K)
 

Mathlib/Algebra/Category/Grp/AB.lean

@@ -31,15 +31,10 @@ noncomputable instance :
     simp only [ShortComplex.ab_exact_iff_ker_le_range] at hS ⊢
     intro x (hx : _ = _)
     dsimp at hx
-    -- The type ascription around `rfl` works around a `HasForget`/`ConcreteCategory` mismatch,
-    -- and should be removed when `Concrete.colimit_exists_rep` takes `ConcreteCategory`.
-    rcases Concrete.colimit_exists_rep S.X₂ x with ⟨j, y, (rfl : (colimit.ι S.X₂ j) y = _)⟩
+    rcases Concrete.colimit_exists_rep S.X₂ x with ⟨j, y, rfl⟩
     rw [← ConcreteCategory.comp_apply, colimMap_eq, colimit.ι_map, ConcreteCategory.comp_apply,
       ← map_zero (colimit.ι S.X₃ j).hom] at hx
-    -- The type ascription around `hk` works around a `HasForget`/`ConcreteCategory` mismatch,
-    -- and should be removed when `Concrete.colimit_exists_rep` takes `ConcreteCategory`.
-    rcases Concrete.colimit_exists_of_rep_eq.{u, u, u} S.X₃ _ _ hx
-      with ⟨k, e₁, e₂, hk : (S.X₃.map e₁) _ = S.X₃.map e₂ 0⟩
+    rcases Concrete.colimit_exists_of_rep_eq.{u, u, u} S.X₃ _ _ hx with ⟨k, e₁, e₂, hk⟩
     rw [map_zero, ← ConcreteCategory.comp_apply, ← NatTrans.naturality, ConcreteCategory.comp_apply]
       at hk
     rcases hS k hk with ⟨t, ht⟩

Mathlib/Algebra/Category/Grp/EpiMono.lean

@@ -64,12 +64,6 @@ open CategoryTheory
 
 namespace Grp
 
-
--- Porting note: already have Group G but Lean can't use that
-@[to_additive]
-instance (G : Grp) : Group G.carrier :=
-  G.str
-
 variable {A B : Grp.{u}} (f : A ⟶ B)
 
 @[to_additive]
@@ -109,7 +103,6 @@ instance : SMul B X' where
     match x with
     | fromCoset y => fromCoset ⟨b • y, by
           rw [← y.2.choose_spec, leftCoset_assoc]
-          -- Porting note: should we make `Bundled.α` reducible?
           let b' : B := y.2.choose
           use b * b'⟩
     | ∞ => ∞
@@ -198,7 +191,6 @@ local notation "g" => g f
 /-- Define `h : B ⟶ S(X')` to be `τ g τ⁻¹`
 -/
 def h : B →* SX' where
-  -- Porting note: mathport removed () from (τ) which are needed
   toFun β := ((τ).symm.trans (g β)).trans τ
   map_one' := by
     ext
@@ -350,10 +342,6 @@ namespace CommGrp
 
 variable {A B : CommGrp.{u}} (f : A ⟶ B)
 
--- Porting note: again to help with non-transparency
-private instance (A : CommGrp) : CommGroup A.carrier := A.str
-private instance (A : CommGrp) : Group A.carrier := A.str.toGroup
-
 @[to_additive]
 theorem ker_eq_bot_of_mono [Mono f] : f.hom.ker = ⊥ :=
   MonoidHom.ker_eq_bot_of_cancel fun u v h => ConcreteCategory.ext_iff.mp <|

Mathlib/Algebra/Category/ModuleCat/Abelian.lean

@@ -76,7 +76,7 @@ instance abelian : Abelian (ModuleCat.{v} R) where
 
 section ReflectsLimits
 
--- Porting note: added to make the following definitions work
+/-- Add this instance to help Lean with universe levels. -/
 instance : HasLimitsOfSize.{v,v} (ModuleCatMax.{v, w} R) :=
   ModuleCat.hasLimitsOfSize.{v, v, max v w}
 

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -286,7 +286,6 @@ def embedding : C ⥤ Free R C where
   map_id _ := rfl
   map_comp {X Y Z} f g := by
     -- Porting note (https://github.com/leanprover-community/mathlib4/pull/10959): simp used to be able to close this goal
-    dsimp only []
     rw [single_comp_single, one_mul]
 
 variable {C} {D : Type u} [Category.{v} D] [Preadditive D] [Linear R D]

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -217,11 +217,6 @@ theorem forget₂_obj (X : ModuleCat R) :
     (forget₂ (ModuleCat R) AddCommGrp).obj X = AddCommGrp.of X :=
   rfl
 
--- Porting note: the simpNF linter correctly doesn't like this.
--- I'm not sure what this is for, actually.
--- If it is really needed, better might be a simp lemma that says
--- `AddCommGrp.of (ModuleCat.of R X) = AddCommGrp.of X`.
--- @[simp 900]
 theorem forget₂_obj_moduleCat_of (X : Type v) [AddCommGroup X] [Module R X] :
     (forget₂ (ModuleCat R) AddCommGrp).obj (of R X) = AddCommGrp.of X :=
   rfl

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -525,8 +525,7 @@ def HomEquiv.toRestriction {X Y} (g : Y ⟶ (coextendScalars f).obj X) :
     (g : Y ⟶ (coextendScalars f).obj X) (y) :
     (HomEquiv.toRestriction f g).hom y = g.hom y (1 : S) := rfl
 
--- Porting note: add to address timeout in unit'
-/-- Auxiliary definition for `unit'` -/
+/-- Auxiliary definition for `unit'`, to address timeouts. -/
 def app' (Y : ModuleCat S) : Y →ₗ[S] (restrictScalars f ⋙ coextendScalars f).obj Y :=
   { toFun := fun y : Y =>
       { toFun := fun s : S => (s • y : Y)
@@ -641,7 +640,8 @@ def HomEquiv.toRestrictScalars {X Y} (g : (extendScalars f).obj X ⟶ Y) :
       letI : Module R S := Module.compHom S f
       letI : Module R Y := Module.compHom Y f
       dsimp
-      erw [RestrictScalars.smul_def, ← LinearMap.map_smul, tmul_smul]
+      rw [RestrictScalars.smul_def, ← LinearMap.map_smul]
+      erw [tmul_smul]
       congr }
 
 -- Porting note: forced to break apart fromExtendScalars due to timeouts
@@ -817,7 +817,6 @@ end ExtendRestrictScalarsAdj
 /-- Given commutative rings `R, S` and a ring hom `f : R →+* S`, the extension and restriction of
 scalars by `f` are adjoint to each other.
 -/
--- @[simps] -- Porting note: removed not in normal form and not used
 def extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
     extendScalars.{u₁,u₂,max v u₂} f ⊣ restrictScalars.{max v u₂,u₁,u₂} f :=
   Adjunction.mk' {

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

@@ -50,7 +50,7 @@ def mk (d : B → M) (d_add : ∀ (b b' : B), d (b + b') = d b + d b' := by simp
     map_add' := d_add
     map_smul' := fun a b ↦ by
       dsimp
-      erw [d_mul, d_map, smul_zero, add_zero]
+      rw [RingHom.smul_toAlgebra, d_mul, d_map, smul_zero, add_zero]
       rfl
     map_one_eq_zero' := by
       dsimp

Mathlib/Algebra/Category/ModuleCat/EpiMono.lean

@@ -58,12 +58,14 @@ instance epi_as_hom''_mkQ (U : Submodule R X) : Epi (ModuleCat.ofHom U.mkQ) :=
 
 instance forget_preservesEpimorphisms : (forget (ModuleCat.{v} R)).PreservesEpimorphisms where
     preserves f hf := by
-      erw [CategoryTheory.epi_iff_surjective, ← epi_iff_surjective]
+      rw [CategoryTheory.epi_iff_surjective, ConcreteCategory.forget_map_eq_coe,
+        ← epi_iff_surjective]
       exact hf
 
 instance forget_preservesMonomorphisms : (forget (ModuleCat.{v} R)).PreservesMonomorphisms where
     preserves f hf := by
-      erw [CategoryTheory.mono_iff_injective, ← mono_iff_injective]
+      rw [CategoryTheory.mono_iff_injective, ConcreteCategory.forget_map_eq_coe,
+        ← mono_iff_injective]
       exact hf
 
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

@@ -175,10 +175,8 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone F) where
 
 instance forget₂AddCommGroup_preservesFilteredColimits :
     PreservesFilteredColimits (forget₂ (ModuleCat.{u} R) AddCommGrp.{u}) where
-  preserves_filtered_colimits J _ _ :=
-  { -- Porting note: without the curly braces for `F`
-    -- here we get a confusing error message about universes.
-    preservesColimit := fun {F : J ⥤ ModuleCat.{u} R} =>
+  preserves_filtered_colimits _ _ _ :=
+  { preservesColimit := fun {F} =>
       preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit F)
         (AddCommGrp.FilteredColimits.colimitCoconeIsColimit
           (F ⋙ forget₂ (ModuleCat.{u} R) AddCommGrp.{u})) }

Mathlib/Algebra/Category/ModuleCat/Kernels.lean

@@ -25,8 +25,7 @@ variable {M N : ModuleCat.{v} R} (f : M ⟶ N)
 
 /-- The kernel cone induced by the concrete kernel. -/
 def kernelCone : KernelFork f :=
-  -- Porting note: previously proven by tidy
-  KernelFork.ofι (ofHom f.hom.ker.subtype) <| by ext x; cases x; assumption
+  KernelFork.ofι (ofHom f.hom.ker.subtype) <| by aesop
 
 /-- The kernel of a linear map is a kernel in the categorical sense. -/
 def kernelIsLimit : IsLimit (kernelCone f) :=
@@ -36,8 +35,8 @@ def kernelIsLimit : IsLimit (kernelCone f) :=
       LinearMap.codRestrict (LinearMap.ker f.hom) (Fork.ι s).hom fun c =>
         LinearMap.mem_ker.2 <| by
           -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
-          erw [← @Function.comp_apply _ _ _ f (Fork.ι s) c, ← LinearMap.coe_comp]
-          rw [← ModuleCat.hom_comp, Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N]
+          erw [← ConcreteCategory.comp_apply]
+          rw [Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N]
           rfl)
     (fun _ => hom_ext <| LinearMap.subtype_comp_codRestrict _ _ _) fun s m h =>
       hom_ext <| LinearMap.ext fun x => Subtype.ext_iff_val.2 (by simp [← h]; rfl)

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

@@ -127,9 +127,7 @@ theorem leftUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
   -- Porting note (https://github.com/leanprover-community/mathlib4/pull/11041): broken ext
   apply TensorProduct.ext
   ext x
-  -- Porting note (https://github.com/leanprover-community/mathlib4/pull/10934): used to be dsimp
-  change ((leftUnitor N).hom) ((tensorHom (𝟙 (of R R)) f) ((1 : R) ⊗ₜ[R] x)) =
-    f (((leftUnitor M).hom) (1 ⊗ₜ[R] x))
+  dsimp
   erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
   rw [LinearMap.map_smul]
   rfl

Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean

@@ -68,13 +68,14 @@ noncomputable def colimitPresheafOfModules : PresheafOfModules R where
   map_id X := colimit.hom_ext (fun j => by
     dsimp
     rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app]
-    erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom),
-      ModuleCat.restrictScalarsId'App_inv_naturality]
-    rw [map_id]
+    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
+    erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom)]
+    rw [ModuleCat.restrictScalarsId'App_inv_naturality, map_id]
     dsimp)
   map_comp {X Y Z} f g := colimit.hom_ext (fun j => by
     dsimp
     rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app, assoc, ι_colimMap_assoc]
+    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
     erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (f ≫ g)).hom),
       ι_preservesColimitIso_inv_assoc (G := ModuleCat.restrictScalars (R.map f).hom)]
     rw [← Functor.map_comp_assoc, ι_colimMap_assoc]

Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean

@@ -73,6 +73,7 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where
     dsimp
     simp only [limMap_π, Functor.comp_obj, evaluation_obj, whiskerLeft_app,
       restriction_app, assoc]
+    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
     erw [preservesLimitIso_hom_π]
     rw [← ModuleCat.restrictScalarsId'App_inv_naturality, map_id,
       ModuleCat.restrictScalarsId'_inv_app]
@@ -85,14 +86,17 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where
     intro j
     simp only [Functor.comp_obj, evaluation_obj, limMap_π, whiskerLeft_app, restriction_app,
       map_comp, ModuleCat.restrictScalarsComp'_inv_app, Functor.map_comp, assoc]
+    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
     erw [preservesLimitIso_hom_π]
     rw [← ModuleCat.restrictScalarsComp'App_inv_naturality]
     dsimp
     rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc, assoc,
       preservesLimitIso_inv_π]
+    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
     erw [limMap_π]
     dsimp
     simp only [Functor.map_comp, assoc, preservesLimitIso_inv_π_assoc]
+    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
     erw [limMap_π_assoc]
     dsimp
 

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -54,7 +54,6 @@ noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
         convert congr_arg LinearMap.range (ModuleCat.hom_ext_iff.mp
             (underlyingIso_arrow (ofHom N.subtype))) using 1
         · have :
-            -- Porting note: added the `.toLinearEquiv.toLinearMap`
             (underlyingIso (ofHom N.subtype)).inv =
               ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
               ext x
@@ -82,36 +81,18 @@ noncomputable def toKernelSubobject {M N : ModuleCat.{v} R} {f : M ⟶ N} :
 theorem toKernelSubobject_arrow {M N : ModuleCat R} {f : M ⟶ N} (x : LinearMap.ker f.hom) :
     (kernelSubobject f).arrow (toKernelSubobject x) = x.1 := by
   -- Porting note (https://github.com/leanprover-community/mathlib4/pull/10959): the whole proof was just `simp [toKernelSubobject]`.
-  suffices ((arrow ((kernelSubobject f))) ∘ (kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = x by
-    convert this
-  rw [Iso.trans_inv, ← LinearMap.coe_comp, ← hom_comp, Category.assoc]
-  simp
+  simp [toKernelSubobject, -hom_comp, ← ConcreteCategory.comp_apply]
 
 /-- An extensionality lemma showing that two elements of a cokernel by an image
 are equal if they differ by an element of the image.
 
 The application is for homology:
 two elements in homology are equal if they differ by a boundary.
 -/
--- Porting note (https://github.com/leanprover-community/mathlib4/pull/11215): TODO compiler complains that this is marked with `@[ext]`.
--- Should this be changed?
--- @[ext] this is no longer an ext lemma under the current interpretation see eg
--- the conversation beginning at
--- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/
--- Goal.20state.20not.20updating.2C.20bugs.2C.20etc.2E/near/338456803
 theorem cokernel_π_imageSubobject_ext {L M N : ModuleCat.{v} R} (f : L ⟶ M) [HasImage f]
     (g : (imageSubobject f : ModuleCat.{v} R) ⟶ N) [HasCokernel g] {x y : N} (l : L)
     (w : x = y + g (factorThruImageSubobject f l)) : cokernel.π g x = cokernel.π g y := by
   subst w
-  -- Porting note (https://github.com/leanprover-community/mathlib4/pull/10959): The proof from here used to just be `simp`.
-  simp only [map_add, add_right_eq_self]
-  -- TODO: add a `@[simp]` lemma along the lines of:
-  -- ```
-  -- lemma ModuleCat.Hom.cokernel_condition : (cokernel.π g).hom (g.hom x) = 0
-  -- ```
-  -- ideally generated for all concrete categories (using a metaprogram like `@[elementwise]`?).
-  -- See also: https://github.com/leanprover-community/mathlib4/pull/19511#discussion_r1867083077
-  change ((factorThruImageSubobject f) ≫ g ≫ (cokernel.π g)).hom l = 0
   simp
 
 end ModuleCat

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -259,11 +259,8 @@ def colimitDesc (t : Cocone F) : colimit.{v, u} F ⟶ t.pt :=
       rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j)
         (IsFiltered.rightToMax i j)]
       dsimp [Types.TypeMax.colimitCoconeIsColimit]
-      rw [MonoidHom.map_mul]
-      -- Porting note: `rw` can't see through coercion is actually forgetful functor,
-      -- so can't rewrite `t.w_apply`
-      congr 1 <;>
-      exact t.w_apply _ _ }
+      rw [MonoidHom.map_mul, t.w_apply, t.w_apply]
+      rfl }
 
 /-- The proposed colimit cocone is a colimit in `MonCat`. -/
 @[to_additive "The proposed colimit cocone is a colimit in `AddMonCat`."]