-- 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 x_1 : G
x_2 :
  (↑(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) (x * x_1))) :
                              C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
                            (f.comp (↑(Homeomorph.mulLeft (x * x_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_2 :
            (↑(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))))
                  _ _ _
                  (HMul.hMul (α :=
                    End (C := TopModuleCat R)
                      (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type 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) x)) :
                              C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
                            (f.comp (↑(Homeomorph.mulLeft x⁻¹) : C(G, G))),
                        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                        ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3) →L[R]
                          ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type 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) x_1)) :
                              C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
                            (f.comp (↑(Homeomorph.mulLeft x_1⁻¹) : C(G, G))),
                        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ :
                        ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3) →L[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_2 :
            (↑(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 [mul_assoc]

Premises used: mul_assoc