no goals
C : Type u
inst✝² : Category C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (leftUnitor X).inv ≫ map (𝟙 (⊤_ C)) f = f ≫ (leftUnitor Y).inv
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]