no goals
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).hom = prod.lift fst snd
apply biprod.hom_ext' <;> apply prod.hom_ext <;> simp [biprod.isoProd]