-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
rep : Action (TopModuleCat.{u_3, u_1} R) G
x :
  (↑(TopModuleCat.toModuleCat (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)))) :
    Type (max u_2 u_3))
a : G
⊢ Eq.{u_3 + 1} (α := (↑rep.V.toModuleCat : Type u_3))
    ((((@ConcreteCategory.hom _ (TopModuleCat.instCategory R)
                  (fun (x1 x2 : TopModuleCat R) ↦
                    (↑x1.toModuleCat : Type (max u_2 u_3)) →L[R] (↑x2.toModuleCat : Type (max u_2 u_3)))
                  (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u_2 u_3)))
                  (fun (X Y : TopModuleCat R) ↦
                    (ContinuousLinearMap.funLike :
                      FunLike ((↑X.toModuleCat : Type (max u_2 u_3)) →L[R] (↑Y.toModuleCat : Type (max u_2 u_3)))
                        (↑X.toModuleCat : Type (max u_2 u_3)) (↑Y.toModuleCat : Type (max u_2 u_3))))
                  _ _ _
                  (TopModuleCat.ofHom
                      {
                        toFun := fun (f : ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)) ↦
                          ContinuousMap.comp
                            (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) 1)) :
                              C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
                            (f.comp (↑(Homeomorph.mulLeft 1⁻¹) : C(G, G))),
                        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } :
                    Quiver.Hom (V := TopModuleCat R)
                      (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)))
                      (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)))) :
                (a : (↑(TopModuleCat.of R C(G, (↑rep.V.toModuleCat : Type u_3))).toModuleCat : Type (max u_2 u_3))) →
                  (↑(TopModuleCat.of R C(G, (↑rep.V.toModuleCat : Type u_3))).toModuleCat : Type (max u_2 u_3)))
              x :
            (↑(TopModuleCat.toModuleCat
                  (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)))) :
              Type (max u_2 u_3))) :
          (a : G) → (↑rep.V.toModuleCat : Type u_3))
        a :
      (↑rep.V.toModuleCat : Type u_3))
    ((((@ConcreteCategory.hom _ (TopModuleCat.instCategory R)
                  (fun (x1 x2 : TopModuleCat R) ↦
                    (↑x1.toModuleCat : Type (max u_2 u_3)) →L[R] (↑x2.toModuleCat : Type (max u_2 u_3)))
                  (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u_2 u_3)))
                  (fun (X Y : TopModuleCat R) ↦
                    (ContinuousLinearMap.funLike :
                      FunLike ((↑X.toModuleCat : Type (max u_2 u_3)) →L[R] (↑Y.toModuleCat : Type (max u_2 u_3)))
                        (↑X.toModuleCat : Type (max u_2 u_3)) (↑Y.toModuleCat : Type (max u_2 u_3))))
                  _ _ _
                  (1 :
                    End (C := TopModuleCat R)
                      (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)))) :
                (a : (↑(TopModuleCat.of R C(G, (↑rep.V.toModuleCat : Type u_3))).toModuleCat : Type (max u_2 u_3))) →
                  (↑(TopModuleCat.of R C(G, (↑rep.V.toModuleCat : Type u_3))).toModuleCat : Type (max u_2 u_3)))
              x :
            (↑(TopModuleCat.toModuleCat
                  (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)))) :
              Type (max u_2 u_3))) :
          (a : G) → (↑rep.V.toModuleCat : Type u_3))
        a :
      (↑rep.V.toModuleCat : Type u_3))

Tactic:
simp