chore: golfing in categories of algebraic objects (#10114)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/Category/AlgebraCat/Basic.lean

@@ -225,8 +225,8 @@ def toAlgEquiv {X Y : AlgebraCat R} (i : X ≅ Y) : X ≃ₐ[R] Y where
     simp only [inv_hom_id]
     -- 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`
+  map_add' := by aesop
+  map_mul' := by aesop
   commutes' := i.hom.commutes -- Porting note: was `by tidy`
 #align category_theory.iso.to_alg_equiv CategoryTheory.Iso.toAlgEquiv
 

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -91,14 +91,13 @@ attribute [coe] ModuleCat.carrier
 
 instance moduleCategory : Category.{v, max (v+1) u} (ModuleCat.{v} R) where
   Hom M N := M →ₗ[R] N
-  id _ := LinearMap.id -- porting note: was `1`
+  id _ := LinearMap.id
   comp f g := g.comp f
   id_comp _ := LinearMap.id_comp _
   comp_id _ := LinearMap.comp_id _
   assoc f g h := LinearMap.comp_assoc (f := f) (g := g) (h := h)
 #align Module.Module_category ModuleCat.moduleCategory
 
--- porting note: was not necessary in mathlib
 instance {M N : ModuleCat.{v} R} : LinearMapClass (M ⟶ N) R M N :=
   LinearMap.semilinearMapClass
 
@@ -120,7 +119,6 @@ instance {M : ModuleCat.{v} R} : AddCommGroup ((forget (ModuleCat R)).obj M) :=
 instance {M : ModuleCat.{v} R} : Module R ((forget (ModuleCat R)).obj M) :=
   (inferInstance : Module R M)
 
--- porting note: added to ease automation
 @[ext]
 lemma ext {M N : ModuleCat.{v} R} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
   DFunLike.ext _ _ h
@@ -273,9 +271,6 @@ def LinearEquiv.toModuleIso {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂
   inv_hom_id := by ext; apply e.right_inv
 #align linear_equiv.to_Module_iso LinearEquiv.toModuleIso
 
--- porting note: for the following three definitions, Lean3 is not able to see that
--- `Module.of R M` is defeq to `M` when `M : Module R`. Lean4 is, so that we no longer
--- need different versions of `LinearEquiv.toModuleIso`.
 /-- Build an isomorphism in the category `Module R` from a `LinearEquiv` between `Module`s. -/
 abbrev LinearEquiv.toModuleIso' {M N : ModuleCat.{v} R} (i : M ≃ₗ[R] N) : M ≅ N :=
   i.toModuleIso
@@ -296,20 +291,8 @@ abbrev LinearEquiv.toModuleIso'Right [AddCommGroup X₁] [Module R X₁] {X₂ :
 namespace CategoryTheory.Iso
 
 /-- Build a `linear_equiv` from an isomorphism in the category `Module R`. -/
-@[simps]
-def toLinearEquiv {X Y : ModuleCat R} (i : X ≅ Y) : X ≃ₗ[R] Y where
-  toFun := i.hom
-  invFun := i.inv
-  left_inv x := by
-    -- porting note: was `by tidy`
-    change (i.hom ≫ i.inv) x = x
-    simp
-  right_inv x := by
-    -- porting note: was `by tidy`
-    change (i.inv ≫ i.hom) x = x
-    simp
-  map_add' := by simp
-  map_smul' := by simp
+def toLinearEquiv {X Y : ModuleCat R} (i : X ≅ Y) : X ≃ₗ[R] Y :=
+  LinearEquiv.ofLinear i.hom i.inv i.inv_hom_id i.hom_inv_id
 #align category_theory.iso.to_linear_equiv CategoryTheory.Iso.toLinearEquiv
 
 end CategoryTheory.Iso
@@ -335,9 +318,6 @@ instance : Preadditive (ModuleCat.{v} R) where
     dsimp
     erw [map_add]
     rfl
-  comp_add P Q R f g g' := by
-    ext
-    rfl
 
 instance forget₂_addCommGroupCat_additive : (forget₂ (ModuleCat.{v} R) AddCommGroupCat).Additive
     where
@@ -355,10 +335,6 @@ instance : Linear S (ModuleCat.{v} S) where
     dsimp
     rw [LinearMap.smul_apply, LinearMap.smul_apply, map_smul]
     rfl
-  comp_smul := by
-    intros
-    ext
-    rfl
 
 variable {X Y X' Y' : ModuleCat.{v} S}
 

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -513,28 +513,14 @@ end RingEquiv
 namespace CategoryTheory.Iso
 
 /-- Build a `RingEquiv` from an isomorphism in the category `RingCat`. -/
-def ringCatIsoToRingEquiv {X Y : RingCat} (i : X ≅ Y) : X ≃+* Y
-    where
-  toFun := i.hom
-  invFun := i.inv
-  -- Porting note: All these proofs were much easier in lean3.
-  left_inv := fun x => show (i.hom ≫ i.inv) x = x by rw [i.hom_inv_id]; rfl
-  right_inv := fun x => show (i.inv ≫ i.hom) x = x by rw [i.inv_hom_id]; rfl
-  map_add' := fun x y => let ii : X →+* Y := i.hom; ii.map_add x y
-  map_mul' := fun x y => let ii : X →+* Y := i.hom; ii.map_mul x y
+def ringCatIsoToRingEquiv {X Y : RingCat} (i : X ≅ Y) : X ≃+* Y :=
+  RingEquiv.ofHomInv i.hom i.inv i.hom_inv_id i.inv_hom_id
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.Ring_iso_to_ring_equiv CategoryTheory.Iso.ringCatIsoToRingEquiv
 
 /-- Build a `RingEquiv` from an isomorphism in the category `CommRingCat`. -/
-def commRingCatIsoToRingEquiv {X Y : CommRingCat} (i : X ≅ Y) : X ≃+* Y
-    where
-  toFun := i.hom
-  invFun := i.inv
-  -- Porting note: All these proofs were much easier in lean3.
-  left_inv := fun x => show (i.hom ≫ i.inv) x = x by rw [i.hom_inv_id]; rfl
-  right_inv := fun x => show (i.inv ≫ i.hom) x = x by rw [i.inv_hom_id]; rfl
-  map_add' := fun x y => let ii : X →+* Y := i.hom; ii.map_add x y
-  map_mul' := fun x y => let ii : X →+* Y := i.hom; ii.map_mul x y
+def commRingCatIsoToRingEquiv {X Y : CommRingCat} (i : X ≅ Y) : X ≃+* Y :=
+  RingEquiv.ofHomInv i.hom i.inv i.hom_inv_id i.inv_hom_id
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.CommRing_iso_to_ring_equiv CategoryTheory.Iso.commRingCatIsoToRingEquiv
 

Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

@@ -143,17 +143,15 @@ def inverseObj (A : AlgebraCat.{u} R) : Mon_ (ModuleCat.{u} R) where
     -- Porting note : `ext` did not pick up `TensorProduct.ext`
     refine TensorProduct.ext <| TensorProduct.ext <| LinearMap.ext fun x => LinearMap.ext fun y =>
       LinearMap.ext fun z => ?_
-    -- Porting note : this `dsimp` does nothing
-    -- dsimp only [AlgebraCat.id_apply, TensorProduct.mk_apply, LinearMap.compr₂_apply,
-    --   Function.comp_apply, ModuleCat.MonoidalCategory.hom_apply, AlgebraCat.coe_comp,
-    --   MonoidalCategory.associator_hom_apply]
-    -- Porting note : because `dsimp` is not effective, `rw` needs to be changed to `erw`
-    rw [compr₂_apply, compr₂_apply, compr₂_apply, compr₂_apply]
+    dsimp only [AlgebraCat.id_apply, TensorProduct.mk_apply, LinearMap.compr₂_apply,
+      Function.comp_apply, ModuleCat.MonoidalCategory.hom_apply, AlgebraCat.coe_comp,
+      MonoidalCategory.associator_hom_apply]
+    rw [compr₂_apply, compr₂_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
     erw [CategoryTheory.comp_apply,
       CategoryTheory.comp_apply, CategoryTheory.comp_apply]
     erw [LinearMap.mul'_apply, LinearMap.mul'_apply]
-    rw [id_apply, TensorProduct.mk_apply]
+    rw [id_apply]
     erw [TensorProduct.mk_apply, TensorProduct.mk_apply, id_apply, LinearMap.mul'_apply,
       LinearMap.mul'_apply]
     simp only [LinearMap.mul'_apply, mul_assoc]
@@ -193,8 +191,7 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgebraCat R where
                 -- Porting note : `ext` did not pick up `TensorProduct.ext`
                 refine TensorProduct.ext ?_
                 dsimp at *
-                rfl
-              one_hom := by ext; rfl }
+                rfl }
           inv :=
             { hom :=
                 { toFun := _root_.id
@@ -204,11 +201,7 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgebraCat R where
                 -- Porting note : `ext` did not pick up `TensorProduct.ext`
                 refine TensorProduct.ext ?_
                 dsimp at *
-                rfl
-              one_hom := by ext; rfl }
-          hom_inv_id := by ext; rfl
-          inv_hom_id := by ext; rfl })
-      (by aesop_cat)
+                rfl } })
   counitIso :=
     NatIso.ofComponents
       (fun A =>
@@ -226,7 +219,6 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgebraCat R where
               map_one' := (algebraMap R A).map_one.symm
               map_mul' := fun x y => (@LinearMap.mul'_apply R _ _ _ _ _ _ x y).symm
               commutes' := fun r => rfl } })
-      (by intros; rfl)
 #align Module.Mon_Module_equivalence_Algebra ModuleCat.monModuleEquivalenceAlgebra
 
 -- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing
@@ -248,7 +240,6 @@ def monModuleEquivalenceAlgebraForget :
           { toFun := _root_.id
             map_add' := fun x y => rfl
             map_smul' := fun c x => rfl } })
-    (by aesop_cat)
 #align Module.Mon_Module_equivalence_Algebra_forget ModuleCat.monModuleEquivalenceAlgebraForget
 
 end ModuleCat