diff --git a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean index f4250bbc6bda2..517b3998efaa0 100644 --- a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean @@ -666,6 +666,7 @@ theorem rightUnitor_monoidal (X₁ X₂ : C) : coherence #align category_theory.right_unitor_monoidal CategoryTheory.rightUnitor_monoidal +set_option maxHeartbeats 400000 in theorem associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) : tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫ (tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =