-- 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_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
⊢ (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
have 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)) sorry) :
                (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)) sorry) :
                (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
            X) ≫
        (functorToContAction F' ⋙ equiv.functor).map f))
Tactic: ext : 2