no goals
C✝¹ : Type u
𝒞 : Category C✝¹
inst✝⁴ : MonoidalCategory C✝¹
C✝ : Type u
inst✝³ : Category C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ (tensorLeftTensor X Y).inv.app Z = (α_ X Y Z).inv
simp [tensorLeftTensor]