-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
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'
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 := ⋯ })
      ({
          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 ⋯
⊢ 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 ⋯

Tactic:
subst h