no goals
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
X Y : C
inst✝ : HasBinaryBiproduct X Y
T U : C
f : T ⟶ X
g : T ⟶ Y
h : X ⟶ U
i : Y ⟶ U
⊢ lift f g ≫ desc h i = f ≫ h + g ≫ i
simp [biprod.lift_eq, biprod.desc_eq]