From a9d54a8a652a6e2325c9d65879250ba40dac6b3c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 19 Aug 2024 11:11:30 +0200 Subject: [PATCH] aesop_cat broke :-( --- Mathlib/CategoryTheory/GradedObject/Monoidal.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean index 0a0e7720c1115..b90d2917ae768 100644 --- a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean +++ b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean @@ -291,7 +291,13 @@ lemma associator_naturality (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ [HasGoodTensor₁₂Tensor X₁ X₂ X₃] [HasGoodTensorTensor₂₃ X₁ X₂ X₃] [HasGoodTensor₁₂Tensor Y₁ Y₂ Y₃] [HasGoodTensorTensor₂₃ Y₁ Y₂ Y₃] : tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom = - (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by aesop_cat + (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by + -- this used to be aesop_cat, but that broke with + -- https://github.com/leanprover/lean4/pull/4154 + ext x i₁ i₂ i₃ h : 2 + simp only [categoryOfGradedObjects_comp, ιTensorObj₃'_tensorHom_assoc, + associator_conjugation, ιTensorObj₃'_associator_hom, assoc, Iso.inv_hom_id_assoc, + ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_tensorHom] end