-- 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
h :
  ∀
    (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))
⊢ @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)))) =
    @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) }))

Tactic:
ext