-- 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 : 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)
this_1 : Continuous v
u : 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) →
  (↑(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_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)) ↦
    (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.obj (P := IsContinuous (FV := FV) (CV := CV)).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.obj (P := IsContinuous (FV := FV) (CV := CV)).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.obj (P := IsContinuous (FV := FV) (CV := CV)).ρ : (a : H) → End X.obj.V) p.1)) :
        (a : (↑((forget₂ V TopCat).obj X.obj.V) : Type u_3)) → (↑((forget₂ V TopCat).obj X.obj.V) : Type u_3))
      p.2
this : Continuous u
⊢ 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 continuous_smul : Continuous (u ∘ v)
Tactic: change Continuous (u ∘ v)