-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, u₁, u₁} C D
inst_5 : F.Additive
X : Mat_ C
i j : X.ι
pos :
  ∀ (h : j = i),
    Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X i))
      (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
          (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
            (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
              Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
                (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
            (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i :
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X i))) :
        F.obj (X.X j) ⟶ F.obj (X.X i))
      (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
          (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i) :
        F.obj (X.X j) ⟶ F.obj (X.X i))
⊢ Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
            Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
          (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i :
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X i))) :
      F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i) :
      F.obj (X.X j) ⟶ F.obj (X.X i))
have neg : ∀ (h : ¬j = i),
  Eq.{v₁ + 1} (α := F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.matrix fun (i j : X.ι) ↦ F.map (CategoryStruct.id.{v₁, max 1 u₁} X i j) :
            Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)))
          (biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i :
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ⟶ F.obj (X.X i))) :
      F.obj (X.X j) ⟶ F.obj (X.X i))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.ι.{0, v₁, u₁} (C := D) (fun (i : X.ι) ↦ F.obj (X.X i)) j)
        (𝟙 (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i)) ≫ biproduct.π (fun (i : X.ι) ↦ F.obj (X.X i)) i) :
      F.obj (X.X j) ⟶ F.obj (X.X i))
Tactic: by_cases h : j = i