-- Module: Mathlib.CategoryTheory.Galois.Equivalence
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 FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F')
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.{w}) ↦
            C((↑X : Type w), (↑Y : Type w))) (CD := TopCat.carrier))
          (Functor.obj (FintypeCat.uSwitchEquivalence.functor.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 w))
    fun
      (p :
        Prod.{u₁, w} (Aut F')
          (↑(Functor.obj
                (forget₂ (Action.{w, w + 1, u₁} 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.{w, w + 1, u₁} FintypeCat (Aut F')) ↦ X.V.obj) TopCat (FD :=
                  fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CD := TopCat.carrier))
                (Functor.obj (FintypeCat.uSwitchEquivalence.functor.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 w)) ↦
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (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.{w}) ↦
              C((↑X : Type w), (↑Y : Type w))) (CD := TopCat.carrier))
            (Functor.obj (FintypeCat.uSwitchEquivalence.functor.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.{w}) ↦
              C((↑X : Type w), (↑Y : Type w))) (CD := TopCat.carrier))
            (Functor.obj (FintypeCat.uSwitchEquivalence.functor.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.{w}) ↦
              C((↑X : Type w), (↑Y : Type w))) (CD := TopCat.carrier))
            (((Functor.obj (FintypeCat.uSwitchEquivalence.functor.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.functor.mapAction (Aut F')).obj X.obj).V)
              p.1)) :
        (a :
            (↑((forget₂ FintypeCat TopCat).obj
                  ((FintypeCat.uSwitchEquivalence.functor.mapAction (Aut F')).obj X.obj).V) :
              Type w)) →
          (↑((forget₂ FintypeCat TopCat).obj ((FintypeCat.uSwitchEquivalence.functor.mapAction (Aut F')).obj X.obj).V) :
            Type w))
      p.2
⊢ (Functor.obj (FintypeCat.uSwitchEquivalence.functor.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)

Tactic:
rw [Action.isContinuous_def]

Premises used: Action.isContinuous_def