no goals
C✝ : Type u
𝒞 : Category C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category C
inst✝ : MonoidalCategory C
U V W X✝ Y Z X X' : C
f : X ⟶ X'
⊢ f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ⊗ 𝟙 tensorUnit')
simp