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
f : X ⟶ Y
⊢ f ⊗ 𝟙 (𝟙_ C) = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv
rw [← rightUnitor_naturality_assoc, Iso.hom_inv_id, Category.comp_id]