From 9e2a933e5b9357cd2b4802f7b02bdea98f580c14 Mon Sep 17 00:00:00 2001
From: Yuma Mizuno <mizuno.y.aj@gmail.com>
Date: Sat, 14 Sep 2024 08:37:00 +0000
Subject: [PATCH] feat(Algebra/Category/AlgebraCat/Monoidal): remove heavy
 defeqs (#16776)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 .../Algebra/Category/AlgebraCat/Monoidal.lean | 35 ++-----------------
 .../LinearAlgebra/TensorProduct/Basic.lean    |  7 ++++
 2 files changed, 10 insertions(+), 32 deletions(-)

diff --git a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
index cd040c2eefb18..9dbed63a629b2 100644
--- a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
+++ b/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. -/
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
index 42c39d96c9f27..98e1a776a8717 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
+++ b/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]