-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X A : C
inst_3 : IsConnected.{u₁, u₂} A
h : Nonempty.{w + 1} (F.obj X).obj
f : X ⟶ A
Z : C
u v : A ⟶ Z
huv : f ≫ u = f ≫ v
⊢ Eq.{w + 1} (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z))
    ((fun (f_1 : A ⟶ Z) ↦
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f_1) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z))
            ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                    (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                    _ _ _ (F.map f) :
                  (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
                (Classical.arbitrary ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))) :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)))
      u)
    ((fun (f_1 : A ⟶ Z) ↦
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f_1) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z))
            ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                    (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                    _ _ _ (F.map f) :
                  (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
                (Classical.arbitrary ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))) :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)))
      v)

Tactic:
simpa using ConcreteCategory.congr_hom (F.congr_map huv) _

Premises used: CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom