From 8120390390977e5508f36130e19195f09b01225c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 19 Aug 2024 10:14:41 +0200 Subject: [PATCH] No rfl after simp needed anymore --- Mathlib/CategoryTheory/GradedObject/Monoidal.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean index 88a32f2bf3bcd..958c61666b838 100644 --- a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean +++ b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean @@ -109,7 +109,6 @@ lemma tensor_id (X Y : GradedObject I C) [HasTensor X Y] : tensorHom (𝟙 X) (𝟙 Y) = 𝟙 _ := by dsimp [tensorHom, mapBifunctorMapMap] simp only [Functor.map_id, NatTrans.id_app, comp_id, mapMap_id] - rfl @[reassoc] lemma tensor_comp {X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃)