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