-- 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
X : Action.{v_1, u_1, u_4} V G
g h : G
x :
  (↑(Functor.obj
        (forget₂ (Action.{v_1, u_1, u_4} V G) (FC := HomSubtype V G (FV := FV) (CV := CV)) (CC :=
          fun (X : Action.{v_1, u_1, u_4} V G) ↦ CV X.V) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
          C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier))
        X) :
    Type u_3)
⊢ (g * h) • x = g • h • x
have change : Eq (α :=
  (↑(Functor.obj.{v_1, u_3, u_1, u_3 + 1}
        (forget₂ 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))
        X.V) :
    Type u_3))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CC := TopCat.carrier)
          (X :=
          Functor.obj.{v_1, u_3, u_1, u_3 + 1}
            (forget₂ 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))
            X.V)
          (Y :=
          Functor.obj.{v_1, u_3, u_1, u_3 + 1}
            (forget₂ 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))
            X.V)
          (CategoryTheory.Functor.map
            (forget₂ 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))
            ((X.ρ : (a : G) → End X.V) (g * h))) :
        (a : (↑((forget₂ V TopCat).obj X.V) : Type u_3)) → (↑((forget₂ V TopCat).obj X.V) : Type u_3))
      x :
    (↑(Functor.obj.{v_1, u_3, u_1, u_3 + 1}
          (forget₂ 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))
          X.V) :
      Type u_3))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CC := TopCat.carrier)
          (X :=
          Functor.obj.{v_1, u_3, u_1, u_3 + 1}
            (forget₂ 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))
            X.V)
          (Y :=
          Functor.obj.{v_1, u_3, u_1, u_3 + 1}
            (forget₂ 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))
            X.V)
          (CategoryStruct.comp (Y :=
            Functor.obj.{v_1, u_3, u_1, u_3 + 1}
              (forget₂ 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))
              X.V)
            (CategoryTheory.Functor.map
              (forget₂ 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))
              ((X.ρ : (a : G) → End X.V) h))
            (CategoryTheory.Functor.map
              (forget₂ 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))
              ((X.ρ : (a : G) → End X.V) g))) :
        (a : (↑((forget₂ V TopCat).obj X.V) : Type u_3)) → (↑((forget₂ V TopCat).obj X.V) : Type u_3))
      x :
    (↑(Functor.obj.{v_1, u_3, u_1, u_3 + 1}
          (forget₂ 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))
          X.V) :
      Type u_3))
Tactic: change (CategoryTheory.forget₂ _ TopCat).map (X.ρ (g * h)) x =
      ((CategoryTheory.forget₂ _ TopCat).map (X.ρ h) ≫
        (CategoryTheory.forget₂ _ TopCat).map (X.ρ g)) x