-- 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.{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')
change :
  Continuous.{u₁, u₁} (X :=
    Aut F' ×
      (FintypeCat.uSwitch.obj
          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).obj)
    (Y :=
    (FintypeCat.uSwitch.obj
        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).obj)
    ((fun
          (p :
            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.obj) ↦
        (Equiv.symm
              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.uSwitchEquiv :
            (a : X.obj.V.obj) → (FintypeCat.uSwitch.obj X.obj.V).obj)
          p) ∘
      (fun
            (p :
              Prod.{u₁, w} (Aut F')
                ((fun (X : Type w) ↦ X)
                  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.obj)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj)
                  ((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 X.obj.V)
                    p.1)) :
              (a : (fun (X : Type w) ↦ X) X.obj.V.obj) → (fun (X : Type w) ↦ X) X.obj.V.obj)
            p.2) ∘
        fun
          (p :
            Aut F' ×
              (FintypeCat.uSwitch.obj
                  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).obj) ↦
        (p.1,
          (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.uSwitchEquiv :
              (a : (FintypeCat.uSwitch.obj X.obj.V).obj) → X.obj.V.obj)
            p.2))
⊢ 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:
change Continuous ((fun p ↦ (FintypeCat.uSwitchEquiv X.obj.V).symm p) ∘
              (fun p : Aut F' × _ ↦ (X.obj.ρ p.1).hom p.2) ∘
              (fun p : Aut F' × _ ↦ (p.1, FintypeCat.uSwitchEquiv _ p.2)))

Premises used: Continuous, CategoryTheory.ConcreteCategory.hom, Function.comp, Prod.mk, CategoryTheory.ObjectProperty.FullSubcategory.obj, Prod.fst, Action.ρ, FintypeCat.uSwitchEquiv, Action.V, CategoryTheory.InducedCategory.Hom.hom, Equiv.symm, Prod.snd, DFunLike.coe