∀ {R : Type u_3} {G : Type u_1} [inst : CommRing R] [inst_1 : Group G] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) (g : G)
  (x x_1 : C(G, ↑rep.V.toModuleCat)),
  (↑(TopModuleCat.Hom.hom (rep.ρ g))).comp ((x + x_1).comp ↑(Homeomorph.mulLeft g⁻¹)) =
    (↑(TopModuleCat.Hom.hom (rep.ρ g))).comp (x.comp ↑(Homeomorph.mulLeft g⁻¹)) +
      (↑(TopModuleCat.Hom.hom (rep.ρ g))).comp (x_1.comp ↑(Homeomorph.mulLeft g⁻¹))