-- 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
⊢ (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

Tactic:
simp [← ofHom_comp, ← ofHom_add, LinearMap.ext_iff]

Premises used: Rep.ofHom_comp, Rep.ofHom_add, LinearMap.ext_iff