-- 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 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
u : A ⟶ X
v : B ⟶ X
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.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 u) :
          (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))
    ((@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 v) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        b :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
refine_2 :
  ∀ (Z : C) (z : (F.obj Z).obj) (isGalois_2 : IsGalois.{u₁, u₂} Z)
    (f :
      (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).obj ⟶
        (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ : 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_1 :
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                  (F.obj (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj))
          (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).pt =
        (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F })).pt),
    True →
      ∀
        (g :
          (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).obj ⟶
            (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ : 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 (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 })).obj)) →
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                    (F.obj (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj))
              (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois_2 : PointedGaloisObject F })).pt =
            (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ : PointedGaloisObject F })).pt),
        ∃ (k : (PointedGaloisObject F)ᵒᵖ) (f :
          Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F } ⟶ k) (g :
          Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F } ⟶ k),
          Eq (α :=
            (fun (X : Type u₂) ↦ X)
              (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) f) :
                  (a :
                      (fun (X : Type u₂) ↦ X)
                        ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                          (Opposite.op { obj := A, pt := a, isGalois := isGalois }))) →
                    (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
                u :
              (fun (X : Type u₂) ↦ X)
                (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) g) :
                  (a :
                      (fun (X : Type u₂) ↦ X)
                        ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                          (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 }))) →
                    (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
                v :
              (fun (X : Type u₂) ↦ X)
                (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
⊢ ∃ (k : (PointedGaloisObject F)ᵒᵖ) (f :
    Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F } ⟶ k) (g :
    Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F } ⟶ k),
    Eq (α :=
      (fun (X : Type u₂) ↦ X)
        (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) f) :
            (a :
                (fun (X : Type u₂) ↦ X)
                  ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                    (Opposite.op { obj := A, pt := a, isGalois := isGalois }))) →
              (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
          u :
        (fun (X : Type u₂) ↦ X)
          (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (map ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) g) :
            (a :
                (fun (X : Type u₂) ↦ X)
                  ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                    (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 }))) →
              (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj k))
          v :
        (fun (X : Type u₂) ↦ X)
          (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))

Tactic:
obtain ⟨⟨Z, z, _⟩, ⟨f, hf⟩, ⟨g, hg⟩, _⟩ :=
      IsFilteredOrEmpty.cocone_objs (C := (PointedGaloisObject F)ᵒᵖ)
        ⟨{ obj := A, pt := a}⟩ ⟨{obj := B, pt := b}⟩

Premises used: Opposite.op, CategoryTheory.IsFilteredOrEmpty.cocone_objs, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk