-- Module: Mathlib.CategoryTheory.Idempotents.Biproducts
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
h :
  (HAdd.hAdd (α :=
        BinaryBicone.pt
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ⟶
          BinaryBicone.pt
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })
        (BinaryBicone.fst
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ≫
          BinaryBicone.inl
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })
        (BinaryBicone.snd
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ≫
          BinaryBicone.inr
            { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
              snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
              inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })).f =
    Hom.f
      (𝟙
        (BinaryBicone.pt
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }))
⊢ HAdd.hAdd (α :=
      BinaryBicone.pt
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
            snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
            inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ⟶
        BinaryBicone.pt
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
            snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
            inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })
      (BinaryBicone.fst
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
            snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
            inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ≫
        BinaryBicone.inl
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
            snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
            inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement })
      (BinaryBicone.snd
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
            snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
            inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement } ≫
        BinaryBicone.inr
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v, u_1} C }, fst := P.decompId_p,
            snd := P.complement.decompId_p, inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯,
            inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : BinaryBicone P P.complement }) =
    𝟙
      (BinaryBicone.pt
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
          inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })

Tactic:
ext