-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ HAdd.hAdd (α :=
      Limits.BinaryBicone.pt (P := A) (Q := B)
          { pt := of (A.ρ.prod B.ρ),
            fst :=
              ofHom
                { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
            snd :=
              ofHom
                { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
            inl :=
              ofHom
                { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inr :=
              ofHom
                { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : Limits.BinaryBicone A B } ⟶
        Limits.BinaryBicone.pt (P := A) (Q := B)
          { pt := of (A.ρ.prod B.ρ),
            fst :=
              ofHom
                { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
            snd :=
              ofHom
                { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
            inl :=
              ofHom
                { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inr :=
              ofHom
                { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : Limits.BinaryBicone A B })
      (Limits.BinaryBicone.fst
          { pt := of (A.ρ.prod B.ρ),
            fst :=
              ofHom
                { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
            snd :=
              ofHom
                { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
            inl :=
              ofHom
                { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inr :=
              ofHom
                { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : Limits.BinaryBicone A B } ≫
        Limits.BinaryBicone.inl
          { pt := of (A.ρ.prod B.ρ),
            fst :=
              ofHom
                { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
            snd :=
              ofHom
                { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
            inl :=
              ofHom
                { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inr :=
              ofHom
                { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : Limits.BinaryBicone A B })
      (Limits.BinaryBicone.snd
          { pt := of (A.ρ.prod B.ρ),
            fst :=
              ofHom
                { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
            snd :=
              ofHom
                { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
            inl :=
              ofHom
                { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inr :=
              ofHom
                { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : Limits.BinaryBicone A B } ≫
        Limits.BinaryBicone.inr
          { pt := of (A.ρ.prod B.ρ),
            fst :=
              ofHom
                { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
            snd :=
              ofHom
                { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
            inl :=
              ofHom
                { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inr :=
              ofHom
                { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
                  B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ : Limits.BinaryBicone A B }) =
    𝟙
      (Limits.BinaryBicone.pt (P := A) (Q := B)
        { pt := of (A.ρ.prod B.ρ),
          fst := ofHom { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ },
          snd := ofHom { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ },
          inl := ofHom { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ },
          inr := ofHom { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ },
          inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ })
have hf : (Hom.hom
      (HAdd.hAdd (α :=
        Limits.BinaryBicone.pt (P := A) (Q := B)
            { pt := of (A.ρ.prod B.ρ),
              fst :=
                ofHom
                  { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
              snd :=
                ofHom
                  { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
              inl :=
                ofHom
                  { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inr :=
                ofHom
                  { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inl_fst := sorry, inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : Limits.BinaryBicone A B } ⟶
          Limits.BinaryBicone.pt (P := A) (Q := B)
            { pt := of (A.ρ.prod B.ρ),
              fst :=
                ofHom
                  { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
              snd :=
                ofHom
                  { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
              inl :=
                ofHom
                  { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inr :=
                ofHom
                  { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inl_fst := sorry, inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : Limits.BinaryBicone A B })
        (Limits.BinaryBicone.fst
            { pt := of (A.ρ.prod B.ρ),
              fst :=
                ofHom
                  { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
              snd :=
                ofHom
                  { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
              inl :=
                ofHom
                  { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inr :=
                ofHom
                  { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inl_fst := sorry, inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : Limits.BinaryBicone A B } ≫
          Limits.BinaryBicone.inl
            { pt := of (A.ρ.prod B.ρ),
              fst :=
                ofHom
                  { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
              snd :=
                ofHom
                  { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
              inl :=
                ofHom
                  { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inr :=
                ofHom
                  { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inl_fst := sorry, inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : Limits.BinaryBicone A B })
        (Limits.BinaryBicone.snd
            { pt := of (A.ρ.prod B.ρ),
              fst :=
                ofHom
                  { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
              snd :=
                ofHom
                  { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
              inl :=
                ofHom
                  { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inr :=
                ofHom
                  { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inl_fst := sorry, inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : Limits.BinaryBicone A B } ≫
          Limits.BinaryBicone.inr
            { pt := of (A.ρ.prod B.ρ),
              fst :=
                ofHom
                  { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
              snd :=
                ofHom
                  { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
              inl :=
                ofHom
                  { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inr :=
                ofHom
                  { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                    B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
              inl_fst := sorry, inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : Limits.BinaryBicone A B }))).toLinearMap =
  (Hom.hom
      (𝟙
        (Limits.BinaryBicone.pt (P := A) (Q := B)
          { pt := of (A.ρ.prod B.ρ),
            fst :=
              ofHom
                { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                  (A.ρ.prod B.ρ).IntertwiningMap A.ρ },
            snd :=
              ofHom
                { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                  (A.ρ.prod B.ρ).IntertwiningMap B.ρ },
            inl :=
              ofHom
                { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                  A.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inr :=
              ofHom
                { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
                  B.ρ.IntertwiningMap (A.ρ.prod B.ρ) },
            inl_fst := sorry, inl_snd := sorry, inr_fst := sorry, inr_snd := sorry : Limits.BinaryBicone A B }))).toLinearMap
Tactic: ext : 2