C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C)).hom ≫ M.one = M.one
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ M.one)) ≫ (λ_ M.X).hom = M.one
slice_lhs 2 3 => rw [leftUnitor_naturality]
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C)).hom ≫ M.one = M.one
simp