-- 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
P : Karoubi.{v, u_1} C
⊢ 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 := ⋯ })
have h : (HAdd.hAdd (α :=
      BinaryBicone.pt
          { pt := { X := P.X, p := 𝟙 P.X, idem := sorry : 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 := sorry,
            inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : BinaryBicone P P.complement } ⟶
        BinaryBicone.pt
          { pt := { X := P.X, p := 𝟙 P.X, idem := sorry : 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 := sorry,
            inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : BinaryBicone P P.complement })
      (BinaryBicone.fst
          { pt := { X := P.X, p := 𝟙 P.X, idem := sorry : 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 := sorry,
            inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : BinaryBicone P P.complement } ≫
        BinaryBicone.inl
          { pt := { X := P.X, p := 𝟙 P.X, idem := sorry : 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 := sorry,
            inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : BinaryBicone P P.complement })
      (BinaryBicone.snd
          { pt := { X := P.X, p := 𝟙 P.X, idem := sorry : 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 := sorry,
            inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : BinaryBicone P P.complement } ≫
        BinaryBicone.inr
          { pt := { X := P.X, p := 𝟙 P.X, idem := sorry : 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 := sorry,
            inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : BinaryBicone P P.complement })).f =
  Hom.f
    (𝟙
      (BinaryBicone.pt
        { pt := { X := P.X, p := 𝟙 P.X, idem := sorry }, fst := P.decompId_p, snd := P.complement.decompId_p,
          inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := sorry, inl_snd := sorry, inr_fst := sorry,
          inr_snd := sorry }))
Tactic: ext