no goals
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
X Y : C
inst✝ : HasBinaryBiproduct X Y
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g = f ≫ inl + g ≫ inr
ext <;> simp [add_comp]