-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
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' := ⋯ :
                      (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 }))).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' := ⋯ :
                    (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 }))).toLinearMap
⊢ 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 := ⋯ })

Tactic:
ext : 2