-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Continuous (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst_1 : (X Y : V) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} V FV (CC := CV)
inst_3 :
  HasForget₂.{u_3, v_1, u_1, u_2, u_3, u_3 + 1, u_3} V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
    C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier)
G : Type u_4
inst_4 : Monoid G
inst_5 : TopologicalSpace G
H : Type u_5
inst_6 : Monoid H
inst_7 : TopologicalSpace H
f f' : G →ₜ* H
h : f = f'
x : ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H
⊢ ∀ (g : G),
    Eq.{v_1 + 1} (α :=
      (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
        (Functor.obj (res V (FV := FV) (CV := CV) f') x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
      (((Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).ρ :
              (a : G) → End ((res V f).obj x).obj.V)
            g ≫
          Iso.hom
            (Iso.refl (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V) :
        (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
          (Functor.obj (res V (FV := FV) (CV := CV) f') x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
      (Iso.hom
            (Iso.refl (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V) ≫
          ((Functor.obj (res V (FV := FV) (CV := CV) f') x).obj (P := IsContinuous (FV := FV) (CV := CV)).ρ :
              (a : G) → End ((res V f').obj x).obj.V)
            g :
        (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
          (Functor.obj (res V (FV := FV) (CV := CV) f') x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
have subst : ∀ (g : G),
  Eq.{v_1 + 1} (α :=
    (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
      (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
    (((Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).ρ :
            (a : G) → End ((res V f).obj x).obj.V)
          g ≫
        Iso.hom
          (Iso.refl (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V) :
      (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
        (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
    (Iso.hom
          (Iso.refl (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V) ≫
        ((Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).ρ :
            (a : G) → End ((res V f).obj x).obj.V)
          g :
      (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
        (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
Tactic: subst h
Cleared hypotheses: f', h