no goals
C : Type u
inst✝² : Category C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f
apply biprod.hom_ext' <;> apply biprod.hom_ext <;>
  simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
    Biprod.inl_ofComponents, Biprod.inr_ofComponents, eq_self_iff_true, Category.assoc,
    comp_zero, biprod.inl_fst, Preadditive.add_comp]