no goals
C : Type u_2
inst✝³ : Category C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst
simp [← Iso.eq_inv_comp]