-- 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
M N : Action (TopModuleCat.{u_3, u_1} R) G
φ : M ⟶ N
g : G
h :
  ∀ (f : (↑(Iobj M).V.toModuleCat : Type (max u_2 u_3))) (g' : G),
    Eq.{u_3 + 1} (α := (↑N.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))))
                    _ (Iobj M).V (Iobj N).V
                    (CategoryStruct.comp (Y := (Iobj M).V) (((Iobj M).ρ : (a : G) → End (Iobj M).V) g : End (Iobj M).V)
                        (TopModuleCat.ofHom (ContinuousLinearMap.compLeftContinuous R G (TopModuleCat.Hom.hom φ.hom)) :
                          Quiver.Hom (V := TopModuleCat R)
                            (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑M.V.toModuleCat : Type u_3)))
                            (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑N.V.toModuleCat : Type u_3)))) :
                      (Iobj M).V ⟶ (Iobj N).V) :
                  (a : (↑(Iobj M).V.toModuleCat : Type (max u_2 u_3))) → (↑(Iobj N).V.toModuleCat : Type (max u_2 u_3)))
                f :
              (↑(Iobj N).V.toModuleCat : Type (max u_2 u_3))) :
            (a : G) → (↑N.V.toModuleCat : Type u_3))
          g' :
        (↑N.V.toModuleCat : Type u_3))
      (((((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat R) ↦
                      (↑x1.toModuleCat : Type (max u_2 u_3)) →L[R] (↑x2.toModuleCat : Type (max u_2 u_3))) (CC :=
                      fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u_2 u_3))) (X := (Iobj M).V) (Y :=
                      (Iobj N).V)
                      (CategoryStruct.comp (Y := (Iobj N).V)
                          (TopModuleCat.ofHom
                              (ContinuousLinearMap.compLeftContinuous R G (TopModuleCat.Hom.hom φ.hom)) :
                            Quiver.Hom (V := TopModuleCat R)
                              (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑M.V.toModuleCat : Type u_3)))
                              (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑N.V.toModuleCat : Type u_3))))
                          (((Iobj N).ρ : (a : G) → End (Iobj N).V) g) :
                        (Iobj M).V ⟶ (Iobj N).V) :
                    (↑(Iobj M).V.toModuleCat : Type (max u_2 u_3)) →L[R]
                      (↑(Iobj N).V.toModuleCat : Type (max u_2 u_3))) :
                  (a : (↑(Iobj M).V.toModuleCat : Type (max u_2 u_3))) → (↑(Iobj N).V.toModuleCat : Type (max u_2 u_3)))
                f :
              (↑(Iobj N).V.toModuleCat : Type (max u_2 u_3))) :
            (a : G) → (↑N.V.toModuleCat : Type u_3))
          g' :
        (↑N.V.toModuleCat : Type u_3))
⊢ Eq (α := (Iobj M).V ⟶ (Iobj N).V)
    (CategoryStruct.comp (Y := (Iobj M).V) (((Iobj M).ρ : (a : G) → End (Iobj M).V) g : End (Iobj M).V)
        (TopModuleCat.ofHom (ContinuousLinearMap.compLeftContinuous R G (TopModuleCat.Hom.hom φ.hom)) :
          Quiver.Hom (V := TopModuleCat R)
            (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑M.V.toModuleCat : Type u_3)))
            (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑N.V.toModuleCat : Type u_3)))) :
      (Iobj M).V ⟶ (Iobj N).V)
    (CategoryStruct.comp (Y := (Iobj N).V)
        (TopModuleCat.ofHom (ContinuousLinearMap.compLeftContinuous R G (TopModuleCat.Hom.hom φ.hom)) :
          Quiver.Hom (V := TopModuleCat R)
            (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑M.V.toModuleCat : Type u_3)))
            (TopModuleCat.of R (ContinuousMap.{u_2, u_3} G (↑N.V.toModuleCat : Type u_3))))
        (((Iobj N).ρ : (a : G) → End (Iobj N).V) g) :
      (Iobj M).V ⟶ (Iobj N).V)

Tactic:
ext f g'