feat(CategoryTheory/ChosenFiniteProducts.lean): simp lemmas for lef…

…t 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

@@ -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`.
 -/