∀ (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] (X : Action (TopModuleCat R) G)
  (x : ↑((ContinuousCohomology.invariants R G).obj X).toModuleCat) (g : G),
  (TopModuleCat.Hom.hom
        ((((HomologicalComplex.asFunctor (ContinuousCohomology.MultiInd.complex R G)).obj X).X
              ((ComplexShape.embeddingUp'Add 1 1).f 0)).ρ
          g))
      ((ContinuousLinearMap.const R G) ↑x) =
    (ContinuousLinearMap.const R G) ↑x