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