-- 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)
⊢ 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))
have rw : 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)
          (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))
            (HMul.hMul (α := End X.V) (β := End X.V) ((X.ρ : (a : G) → End X.V) g : End X.V)
              ((X.ρ : (a : G) → End X.V) h : End X.V))) :
        (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)
          (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))
            (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → End X.V) h) ((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: rw [← Functor.map_comp, map_mul]