{A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {inst : CommRing A} →
          {inst_1 : Monoid G} →
            {inst_2 : AddCommMonoid V} →
              {inst_3 : AddCommMonoid W} →
                {inst_4 : Module A V} →
                  {inst_5 : Module A W} →
                    {ρ : Representation A G V} →
                      {σ : Representation A G W} →
                        {P : Sort u} →
                          {toLinearMap : V →ₗ[A] W} →
                            {isIntertwining' :
                                ∀ (g : G) (v : V), toLinearMap.toFun ((ρ g) v) = (σ g) (toLinearMap.toFun v)} →
                              {toLinearMap' : V →ₗ[A] W} →
                                {isIntertwining'' :
                                    ∀ (g : G) (v : V), toLinearMap'.toFun ((ρ g) v) = (σ g) (toLinearMap'.toFun v)} →
                                  { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' } =
                                      { toLinearMap := toLinearMap', isIntertwining' := isIntertwining'' } →
                                    (toLinearMap ≍ toLinearMap' → P) → P