-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst_3 : IsIso f₁₁
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
              (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
              (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
                  (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
                  (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
                biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) biprod.inl (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)))
      biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
              (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
              (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
                  (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
                  (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
                biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) biprod.inl (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)))
      biprod.snd
⊢ Eq (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
        (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
        (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
            (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
            (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
have h₂ : CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
        (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
            (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
            (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
                (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
                (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
              biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) biprod.inr (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂))) biprod.fst
Tactic: ext