feat(Algebra/Category/AlgebraCat/Monoidal): remove heavy defeqs (#16776)

Remove heavy defeqs detected in [zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Heavy.20rfl).

Alternatives for `forget₂_map_associator_hom` and `forget₂_map_associator_inv` are provided in #16778.

Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

@@ -55,43 +55,14 @@ instance : MonoidalCategoryStruct (AlgebraCat.{u} R) where
   leftUnitor X := (Algebra.TensorProduct.lid R X).toAlgebraIso
   rightUnitor X := (Algebra.TensorProduct.rid R R X).toAlgebraIso
 
-theorem forget₂_map_associator_hom (X Y Z : AlgebraCat.{u} R) :
-    (forget₂ (AlgebraCat R) (ModuleCat R)).map (α_ X Y Z).hom =
-      (α_
-        (forget₂ _ (ModuleCat R) |>.obj X)
-        (forget₂ _ (ModuleCat R) |>.obj Y)
-        (forget₂ _ (ModuleCat R) |>.obj Z)).hom := by
-  rfl
-
-theorem forget₂_map_associator_inv (X Y Z : AlgebraCat.{u} R) :
-    (forget₂ (AlgebraCat R) (ModuleCat R)).map (α_ X Y Z).inv =
-      (α_
-        (forget₂ _ (ModuleCat R) |>.obj X)
-        (forget₂ _ (ModuleCat R) |>.obj Y)
-        (forget₂ _ (ModuleCat R) |>.obj Z)).inv := by
-  rfl
-
-set_option maxHeartbeats 800000 in
 noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R) :=
   Monoidal.induced
     (forget₂ (AlgebraCat R) (ModuleCat R))
     { μIso := fun X Y => Iso.refl _
       εIso := Iso.refl _
-      associator_eq := fun X Y Z => by
-        dsimp only [forget₂_module_obj, forget₂_map_associator_hom]
-        simp only [eqToIso_refl, Iso.refl_trans, Iso.refl_symm, Iso.trans_hom,
-          MonoidalCategory.tensorIso_hom, Iso.refl_hom, MonoidalCategory.tensor_id]
-        erw [Category.id_comp, Category.comp_id, MonoidalCategory.tensor_id, Category.id_comp]
-      leftUnitor_eq := fun X => by
-        dsimp only [forget₂_module_obj, forget₂_module_map, Iso.refl_symm, Iso.trans_hom,
-          Iso.refl_hom, MonoidalCategory.tensorIso_hom]
-        erw [Category.id_comp, MonoidalCategory.tensor_id, Category.id_comp]
-        rfl
-      rightUnitor_eq := fun X => by
-        dsimp
-        erw [Category.id_comp, MonoidalCategory.tensor_id, Category.id_comp]
-        exact congr_arg LinearEquiv.toLinearMap <|
-          TensorProduct.AlgebraTensorModule.rid_eq_rid R X }
+      associator_eq := fun X Y Z => TensorProduct.ext₃ (fun x y z => rfl)
+      leftUnitor_eq := fun X => TensorProduct.ext' (fun x y => rfl)
+      rightUnitor_eq := fun X => TensorProduct.ext' (fun x y => rfl) }
 
 variable (R) in
 /-- `forget₂ (AlgebraCat R) (ModuleCat R)` as a monoidal functor. -/

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -526,6 +526,13 @@ theorem ext' {g h : M ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x
     TensorProduct.induction_on z (by simp_rw [LinearMap.map_zero]) H fun x y ihx ihy => by
       rw [g.map_add, h.map_add, ihx, ihy]
 
+theorem ext₃ {g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q}
+    (H : ∀ x y z, g (x ⊗ₜ y ⊗ₜ z) = h (x ⊗ₜ y ⊗ₜ z)) : g = h :=
+  ext' fun x => TensorProduct.induction_on x
+    (fun x => by simp only [zero_tmul, map_zero])
+    (fun x y => H x y)
+    (fun x y ihx ihy z => by rw [add_tmul, g.map_add, h.map_add, ihx, ihy])
+
 theorem lift.unique {g : M ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = f x y) : g = lift f :=
   ext' fun m n => by rw [H, lift.tmul]