∀ {R' : Type u_5} {E : Type u_6} [inst : CommSemiring R'] [inst_1 : StarRing R'] [inst_2 : NonUnitalNonAssocSemiring E]
  [inst_3 : StarRing E] [inst_4 : Module R' E] [inst_5 : StarModule R' E] [inst_6 : SMulCommClass R' E E]
  [inst_7 : IsScalarTower R' E E],
  star (WithConv.toConv (LinearMap.mul' R' E)) = WithConv.toConv (LinearMap.mul' R' E ∘ₗ ↑(TensorProduct.comm R' E E))