no goals
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoCoprod X Y).inv = coprod.desc inl inr
apply biprod.hom_ext <;> apply coprod.hom_ext <;> simp [biprod.isoCoprod]