From 6a98dbda3b518bc41f99919309f3571fe4f7a637 Mon Sep 17 00:00:00 2001 From: Robin Carlier Date: Sun, 13 Oct 2024 17:05:05 +0000 Subject: [PATCH] feat(CategoryTheory/ChosenFiniteProducts.lean): `simp` lemmas for left and right unitors in `ChosenFiniteProducts` monoidal structure (#17695) Add 4 `simp` lemmas for left and right unitors in the monoidal structure obtained from instances of `ChosenFiniteProducts`. --- Mathlib/CategoryTheory/ChosenFiniteProducts.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean index 7ae5f97b5511b..4c342ebe1413b 100644 --- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean +++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean @@ -178,6 +178,22 @@ lemma associator_inv_fst_snd (X Y Z : C) : lemma associator_inv_snd (X Y Z : C) : (α_ X Y Z).inv ≫ snd _ _ = snd _ _ ≫ snd _ _ := lift_snd _ _ +@[reassoc (attr := simp)] +lemma leftUnitor_inv_fst (X : C) : + (λ_ X).inv ≫ fst _ _ = toUnit _ := toUnit_unique _ _ + +@[reassoc (attr := simp)] +lemma leftUnitor_inv_snd (X : C) : + (λ_ X).inv ≫ snd _ _ = 𝟙 X := lift_snd _ _ + +@[reassoc (attr := simp)] +lemma rightUnitor_inv_fst (X : C) : + (ρ_ X).inv ≫ fst _ _ = 𝟙 X := lift_fst _ _ + +@[reassoc (attr := simp)] +lemma rightUnitor_inv_snd (X : C) : + (ρ_ X).inv ≫ snd _ _ = toUnit _ := toUnit_unique _ _ + /-- Construct an instance of `ChosenFiniteProducts C` given an instance of `HasFiniteProducts C`. -/