∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
  (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) [inst_3 : CategoryTheory.IsIso f₁₁],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Biprod.unipotentLower (-CategoryTheory.CategoryStruct.comp f₂₁ (CategoryTheory.inv f₁₁))).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
        (CategoryTheory.Biprod.unipotentUpper (-CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f₁₁) f₁₂)).hom) =
    CategoryTheory.Limits.biprod.map f₁₁
      (f₂₂ - CategoryTheory.CategoryStruct.comp f₂₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f₁₁) f₁₂))