-- Module: Mathlib.CategoryTheory.Action.Continuous
Goal:
V_1 : Type u_1
inst : Category.{v_1, u_1} V_1
FV_1 : V_1 → V_1 → Type u_2
CV_1 : V_1 → Type u_3
inst_1 : (X Y : V_1) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FV_1 X Y) (CV_1 X) (CV_1 Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} V_1 FV_1 (CC := CV_1)
inst_3 :
  HasForget₂.{u_3, v_1, u_1, u_2, u_3, u_3 + 1, u_3} V_1 (FC := FV_1) (CC := CV_1) TopCat (FD :=
    fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier)
G_1 : Type u_4
inst_4 : Monoid G_1
inst_5 : TopologicalSpace G_1
V : Type u_5
W : Type u_6
inst_6 : Category.{v_2, u_5} V
FV : V → V → Type u_7
CV : V → Type u_8
inst_7 : (X Y : V) → FunLike.{u_7 + 1, u_8 + 1, u_8 + 1} (FV X Y) (CV X) (CV Y)
inst_8 : ConcreteCategory.{u_8, v_2, u_5, u_7} V FV (CC := CV)
inst_9 :
  HasForget₂.{u_8, v_2, u_5, u_7, u_8, u_8 + 1, u_8} V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_8}) ↦
    C((↑X : Type u_8), (↑Y : Type u_8))) (CD := TopCat.carrier)
inst_10 : Category.{v_3, u_6} W
FW : W → W → Type u_9
CW : W → Type u_10
inst_11 : (X Y : W) → FunLike.{u_9 + 1, u_10 + 1, u_10 + 1} (FW X Y) (CW X) (CW Y)
inst_12 : ConcreteCategory.{u_10, v_3, u_6, u_9} W FW (CC := CW)
inst_13 :
  HasForget₂.{u_10, v_3, u_6, u_9, u_10, u_10 + 1, u_10} W (FC := FW) (CC := CW) TopCat (FD :=
    fun (X Y : TopCat.{u_10}) ↦ C((↑X : Type u_10), (↑Y : Type u_10))) (CD := TopCat.carrier)
G : Type u_11
inst_14 : Monoid G
inst_15 : TopologicalSpace G
F F' : Functor.{v_2, v_3, u_5, u_6} V W
e : F ≅ F'
H :
  ∀ (X : ContAction.{v_2, u_5, u_7, u_8, u_11} V (FV := FV) (CV := CV) G),
    (obj (F.mapAction G) (X.obj (P := IsContinuous (FV := FV) (CV := CV)))).IsContinuous (FV := FW) (CV := CW)
H' :
  ∀ (X : ContAction.{v_2, u_5, u_7, u_8, u_11} V (FV := FV) (CV := CV) G),
    (obj (F'.mapAction G) (X.obj (P := IsContinuous (FV := FV) (CV := CV)))).IsContinuous (FV := FW) (CV := CW)
X : ContAction.{v_2, u_5, u_7, u_8, u_11} V (FV := FV) (CV := CV) G
⊢ ∀ (g : G),
    Eq.{v_3 + 1} (α :=
      ((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F H).obj X).obj (P :=
            IsContinuous (FV := FW) (CV := CW)).V ⟶
        ((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F' H').obj X).obj (P :=
            IsContinuous (FV := FW) (CV := CW)).V)
      ((((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F H).obj X).obj (P :=
                  IsContinuous (FV := FW) (CV := CW)).ρ :
              (a : G) → End ((mapContAction G F H).obj X).obj.V)
            g ≫
          Iso.hom (e.app X.obj (P := IsContinuous (FV := FV) (CV := CV)).V) :
        ((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F H).obj X).obj (P :=
              IsContinuous (FV := FW) (CV := CW)).V ⟶
          ((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F' H').obj X).obj (P :=
              IsContinuous (FV := FW) (CV := CW)).V)
      (Iso.hom (e.app X.obj (P := IsContinuous (FV := FV) (CV := CV)).V) ≫
          (((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F' H').obj X).obj (P :=
                  IsContinuous (FV := FW) (CV := CW)).ρ :
              (a : G) → End ((mapContAction G F' H').obj X).obj.V)
            g :
        ((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F H).obj X).obj (P :=
              IsContinuous (FV := FW) (CV := CW)).V ⟶
          ((mapContAction (FV := FV) (CV := CV) (FW := FW) (CW := CW) G F' H').obj X).obj (P :=
              IsContinuous (FV := FW) (CV := CW)).V)

Tactic:
simp