no goals
𝒜 : Type u_1
inst✝² : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ f ≫ g = 0
rw [← h.inl_comp_iso_eq, Category.assoc, h.iso_comp_eq_snd, biprod.inl_snd]