-- 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')
⊢ 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))

Tactic:
exact Continuous.comp (by fun_prop) (Continuous.comp X.2.1 (by fun_prop))

Premises used: Continuous.comp, ContinuousSMul.continuous_smul