-- 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
⊢ 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)
have 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))
Tactic: ext f g'