-- 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
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 ⋯
have pos : 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)) =
  eqToHom sorry
Tactic: subst h
Cleared hypotheses: j', h