∀ {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₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂),
  ((L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
      (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×'
        (g₂₂ : X₂ ⟶ Y₂) ×'
          CategoryTheory.CategoryStruct.comp L.hom
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Biprod.ofComponents
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
                    (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
                    (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd))
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
                    (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
                    (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)))
                R.hom) =
            CategoryTheory.Limits.biprod.map
              (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
                (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
              g₂₂) =
    ((L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
      (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×'
        (g₂₂ : X₂ ⟶ Y₂) ×'
          CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp f R.hom) =
            CategoryTheory.Limits.biprod.map
              (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
                (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
              g₂₂)