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).inv = lift prod.fst prod.snd
apply biprod.hom_ext <;> simp [Iso.inv_comp_eq]