-- Lean 4 proof step from Mathlib.Algebra.Category.ContinuousCohomology.Basic (goal)
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
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))
have h : Eq (α := (↑N.V.toModuleCat : Type u_3))
  ((TopModuleCat.Hom.hom ((M.ρ : (a : G) → End M.V) g ≫ φ.hom) :
        (a : (↑M.V.toModuleCat : Type u_3)) → (↑N.V.toModuleCat : Type u_3))
      ((f : (a : G) → (↑M.V.toModuleCat : Type u_3)) (g⁻¹ * g') : (↑M.V.toModuleCat : Type u_3)) :
    (↑N.V.toModuleCat : Type u_3))
  ((TopModuleCat.Hom.hom (φ.hom ≫ (N.ρ : (a : G) → End N.V) g) :
        (a : (↑M.V.toModuleCat : Type u_3)) → (↑N.V.toModuleCat : Type u_3))
      ((f : (a : G) → (↑M.V.toModuleCat : Type u_3)) (g⁻¹ * g') : (↑M.V.toModuleCat : Type u_3)) :
    (↑N.V.toModuleCat : Type u_3))
Tactic: change (M.ρ g ≫ φ.hom).hom (f (g⁻¹ * g')) = (φ.hom ≫ N.ρ g).hom (f (g⁻¹ * g'))