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 Y : C
⊢ (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ (𝟙 X ⊗ (ρ_ Y).hom)
rw [← tensor_right_iff, comp_tensor_id, ← cancel_mono (α_ X Y (𝟙_ C)).hom, assoc,
  associator_naturality, ← triangle_assoc, ← triangle, id_tensor_comp, pentagon_assoc, ←
  associator_naturality, tensor_id]