-- 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_1 : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : 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') ≌
  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) :=
  Equivalence.trans
    (Equivalence.mapContAction (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FW :=
      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CW :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯)
    (ContAction.resEquiv FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) f_1)
X Y : C
f : X ⟶ Y
h :
  Action.Hom.hom
      (InducedCategory.Hom.hom
        ((functorToContAction F).map f ≫
          Iso.hom
            ((fun (X : C) ↦
                (ObjectProperty.isoMk
                    (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
                  (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
              Y))) =
    Action.Hom.hom
      (InducedCategory.Hom.hom
        (Iso.hom
            ((fun (X : C) ↦
                (ObjectProperty.isoMk
                    (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
                  (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
              X) ≫
          (functorToContAction F' ⋙ equiv.functor).map f))
⊢ (functorToContAction F).map f ≫
      Iso.hom
        ((fun (X : C) ↦
            (ObjectProperty.isoMk
                (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
              (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
          Y) =
    Iso.hom
        ((fun (X : C) ↦
            (ObjectProperty.isoMk
                (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
              (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
          X) ≫
      (functorToContAction F' ⋙ equiv.functor).map f

Tactic:
ext : 2