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✝¹
C✝ : Type u
inst✝³ : Category C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ (tensorRightTensor X Y).inv.app Z = (α_ Z X Y).hom
simp [tensorRightTensor]