-- Module: Mathlib.CategoryTheory.Galois.Decomposition
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
G : Functor.{u₂, w, u₁, w + 1} C FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois.{u₁, u₂} X], t.app X = s.app X
X : C
x : (F.obj X).obj
w :
  ∀ (A : C) (f : A ⟶ X) (a : (F.obj A).obj),
    IsGalois.{u₁, u₂} A →
      Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
        ((@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))
                _ _ _ (t.app X) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
            ((@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 A)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
        ((@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))
                _ _ _ (s.app X) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
            ((@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 A)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
    ((@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))
            _ _ _ (t.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
    ((@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))
            _ _ _ (s.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))

Tactic:
obtain ⟨A, f, a, _, rfl⟩ := exists_hom_from_galois_of_fiber F X x

Premises used: CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber, rfl