-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Equivalence (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X :
  ContAction.{w, w + 1, w, w, u₁} FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F')
⊢ (Functor.obj (FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F'))
        (X.obj (P :=
          Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)))).IsContinuous
    (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
have rw : Continuous (Y :=
  (↑(Functor.obj
        (forget₂ FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
          fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) TopCat (FD := fun (X Y : TopCat.{u₁}) ↦
          C((↑X : Type u₁), (↑Y : Type u₁))) (CD := TopCat.carrier))
        (Functor.obj (FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F'))
            (X.obj (P :=
              Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)))).V) :
    Type u₁))
  fun
    (p :
      Aut F' ×
        (↑(Functor.obj
              (forget₂ (Action FintypeCat (Aut F')) (FC :=
                Action.HomSubtype FintypeCat (Aut F') (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                (CC := fun (X : Action FintypeCat (Aut F')) ↦ X.V.obj) TopCat (FD := fun (X Y : TopCat.{u₁}) ↦
                C((↑X : Type u₁), (↑Y : Type u₁))) (CD := TopCat.carrier))
              (Functor.obj (FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F'))
                (X.obj (P :=
                  Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))))) :
          Type u₁)) ↦
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u₁}) ↦ C((↑X : Type u₁), (↑Y : Type u₁))) (CC := TopCat.carrier) (X :=
        Functor.obj
          (forget₂ FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) TopCat (FD := fun (X Y : TopCat.{u₁}) ↦
            C((↑X : Type u₁), (↑Y : Type u₁))) (CD := TopCat.carrier))
          (Functor.obj (FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F'))
              (X.obj (P :=
                Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)))).V)
        (Y :=
        Functor.obj
          (forget₂ FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) TopCat (FD := fun (X Y : TopCat.{u₁}) ↦
            C((↑X : Type u₁), (↑Y : Type u₁))) (CD := TopCat.carrier))
          (Functor.obj (FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F'))
              (X.obj (P :=
                Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)))).V)
        (Functor.map
          (forget₂ FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) TopCat (FD := fun (X Y : TopCat.{u₁}) ↦
            C((↑X : Type u₁), (↑Y : Type u₁))) (CD := TopCat.carrier))
          (((Functor.obj (FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F'))
                  (X.obj (P :=
                    Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)))).ρ :
              (a : Aut F') → End ((FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F')).obj X.obj).V)
            p.1)) :
      (a :
          (↑((forget₂ FintypeCat TopCat).obj ((FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F')).obj X.obj).V) :
            Type u₁)) →
        (↑((forget₂ FintypeCat TopCat).obj ((FintypeCat.uSwitchEquivalence.inverse.mapAction (Aut F')).obj X.obj).V) :
          Type u₁))
    p.2
Tactic: rw [Action.isContinuous_def]