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