-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat
inst_2 : FiberFunctor F
x x_1 : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois : IsGalois.{u₁, u₂} A
B : C
b : (F.obj B).obj
isGalois_1 : IsGalois.{u₁, u₂} B
x_2 x_3 :
  { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F } ⟶ { obj := B, pt := b, isGalois := isGalois_1 }
f :
  { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.obj ⟶
    { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }.obj
hf :
  (@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 { obj := A, pt := a, isGalois := isGalois }.obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj { obj := B, pt := b, isGalois := isGalois_1 }.obj))
      { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.pt =
    { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }.pt
g :
  { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.obj ⟶
    { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }.obj
hg :
  (@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 g) :
        (a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj { obj := A, pt := a, isGalois := isGalois }.obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj { obj := B, pt := b, isGalois := isGalois_1 }.obj))
      { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.pt =
    { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }.pt
Z : C
h : Z ⟶ A
z : (F.obj Z).obj
hgal : IsGalois.{u₁, u₂} Z
hhz :
  (@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 h) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      z =
    a
a₁ :
  Eq.{u₂ + 1} (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
    ((fun (f : Z ⟶ B) ↦
        ((@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 Z)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            z :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)))
      (Hom.val
        ({ val := h, comp := hhz } ≫
          { val := f, comp := hf :
            { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.Hom
              { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F } })))
    ((fun (f : Z ⟶ B) ↦
        ((@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 Z)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            z :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)))
      (Hom.val
        ({ val := h, comp := hhz } ≫
          { val := g, comp := hg :
            { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.Hom
              { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F } })))
⊢ Eq.{u₂ + 1} (α :=
    { obj := Z, pt := z, isGalois := hgal : PointedGaloisObject F }.obj ⟶
      { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }.obj)
    (Hom.val
      ({ val := h, comp := hhz } ≫
        { val := f, comp := hf :
          { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.Hom
            { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F } }))
    (Hom.val
      ({ val := h, comp := hhz } ≫
        { val := g, comp := hg :
          { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.Hom
            { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F } }))

Tactic:
apply evaluation_injective_of_isConnected F Z B z

Premises used: CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected