-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
inst_2 : HasFiniteBiproducts.{v, u_1} C
J : Type
inst_3 : Finite J
F : J → Karoubi.{v, u_1} C
j j' : J
pos :
  ∀ (h : j = j'),
    CategoryStruct.comp (Y :=
        { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
          p :=
            (biproduct.map fun (j : J) ↦ (F j).p :
              Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
          idem := ⋯ })
        ({
            f :=
              CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j) (biproduct.map fun (j : J) ↦ (F j).p),
            comm := ⋯ } :
          (F j).Hom
            { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
              p :=
                (biproduct.map fun (j : J) ↦ (F j).p :
                  Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                    (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
              idem := ⋯ })
        ({
            f :=
              CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                (biproduct.map fun (j : J) ↦ (F j).p) (Bicone.π (biproduct.bicone fun (j : J) ↦ (F j).X) j'),
            comm := ⋯ } :
          { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
                p :=
                  (biproduct.map fun (j : J) ↦ (F j).p :
                    Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                      (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
                idem := ⋯ : Karoubi.{v, u_1} C }.Hom
            (F j')) =
      eqToHom ⋯
⊢ Eq.{v + 1} (α := F j ⟶ F j')
    (CategoryStruct.comp (Y :=
      { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
        p :=
          (biproduct.map fun (j : J) ↦ (F j).p :
            Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
        idem := ⋯ })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j) (biproduct.map fun (j : J) ↦ (F j).p),
          comm := ⋯ } :
        (F j).Hom
          { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := ⋯ })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
              (Bicone.π (biproduct.bicone fun (j : J) ↦ (F j).X) j'),
          comm := ⋯ } :
        { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
              p :=
                (biproduct.map fun (j : J) ↦ (F j).p :
                  Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                    (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
              idem := ⋯ : Karoubi.{v, u_1} C }.Hom
          (F j')))
    (if h : j = j' then eqToHom ⋯ else 0)
have neg : ∀ (h : ¬j = j'),
  Eq.{v + 1} (α := F j ⟶ F j')
    (CategoryStruct.comp (Y :=
      { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
        p :=
          (biproduct.map fun (j : J) ↦ (F j).p :
            Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
        idem := sorry })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
              (biproduct.ι.{0, v, u_1} (C := C) (fun (j : J) ↦ (F j).X) j) (biproduct.map fun (j : J) ↦ (F j).p),
          comm := sorry } :
        (F j).Hom
          { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
            p :=
              (biproduct.map fun (j : J) ↦ (F j).p :
                Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                  (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
            idem := sorry })
      ({
          f :=
            CategoryStruct.comp (Y := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X) (biproduct.map fun (j : J) ↦ (F j).p)
              (Bicone.π (biproduct.bicone fun (j : J) ↦ (F j).X) j'),
          comm := sorry } :
        { X := biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X,
              p :=
                (biproduct.map fun (j : J) ↦ (F j).p :
                  Quiver.Hom.{v, u_1} (V := C) (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)
                    (biproduct.{0, v, u_1} fun (j : J) ↦ (F j).X)),
              idem := sorry : Karoubi.{v, u_1} C }.Hom
          (F j')))
    0
Tactic: split_ifs with h