-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Continuous (hypothesis)
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 : G →ₜ* H
X : ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H
v : Prod.{u_4, u_3} G
    (↑(Functor.obj
          (forget₂ (ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H) (FC :=
            fun
              (X Y :
                ObjectProperty.FullSubcategory (C := Action.{v_1, u_1, u_5} V H) (IsContinuous (FV := FV) (CV := CV))) ↦
            HomSubtype V H (FV := FV) (CV := CV) (X.obj (P := IsContinuous (FV := FV) (CV := CV)))
              (Y.obj (P := IsContinuous (FV := FV) (CV := CV))))
            (CC :=
            fun
              (X :
                ObjectProperty.FullSubcategory (C := Action.{v_1, u_1, u_5} V H) (IsContinuous (FV := FV) (CV := CV))) ↦
            CV X.obj (P := IsContinuous (FV := FV) (CV := CV)).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) →
  Prod.{u_5, u_3} H
    (↑(Functor.obj
          (forget₂ (ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H) (FC :=
            fun
              (X Y :
                ObjectProperty.FullSubcategory (C := Action.{v_1, u_1, u_5} V H) (IsContinuous (FV := FV) (CV := CV))) ↦
            HomSubtype V H (FV := FV) (CV := CV) (X.obj (P := IsContinuous (FV := FV) (CV := CV)))
              (Y.obj (P := IsContinuous (FV := FV) (CV := CV))))
            (CC :=
            fun
              (X :
                ObjectProperty.FullSubcategory (C := Action.{v_1, u_1, u_5} V H) (IsContinuous (FV := FV) (CV := CV))) ↦
            CV X.obj (P := IsContinuous (FV := FV) (CV := CV)).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) :=
  fun
      (p :
        Prod.{u_4, u_3} G
          (↑(Functor.obj
                (forget₂ (ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H) (FC :=
                  fun
                    (X Y :
                      ObjectProperty.FullSubcategory (C := Action.{v_1, u_1, u_5} V H)
                        (IsContinuous (FV := FV) (CV := CV))) ↦
                  HomSubtype V H (FV := FV) (CV := CV) (X.obj (P := IsContinuous (FV := FV) (CV := CV)))
                    (Y.obj (P := IsContinuous (FV := FV) (CV := CV))))
                  (CC :=
                  fun
                    (X :
                      ObjectProperty.FullSubcategory (C := Action.{v_1, u_1, u_5} V H)
                        (IsContinuous (FV := FV) (CV := CV))) ↦
                  CV X.obj (P := IsContinuous (FV := FV) (CV := CV)).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)) ↦
    ((f : (a : G) → H) p.1, p.2)
⊢ Continuous (Y :=
    (↑(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))
          (Functor.obj (ObjectProperty.ι (IsContinuous (FV := FV) (CV := CV)) ⋙ Action.res V (↑f : G →* H)) X)) :
      Type u_3))
    fun
      (p :
        Prod.{u_4, u_3} G
          (↑(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))
                (Functor.obj (ObjectProperty.ι (IsContinuous (FV := FV) (CV := CV)) ⋙ Action.res V (↑f : G →* H)) X)) :
            Type u_3)) ↦
    p.1 • p.2
have this : Continuous v
Tactic: have : Continuous v := by fun_prop