-- 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
refine_2 :
  ∀ (v : B ⟶ X),
    Eq (α :=
        (fun (X : Type u₂) ↦ X)
          (Functor.obj
            (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
              (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
            (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
                  (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })) :
              (a_1 :
                  (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)
                  (((const (PointedGaloisObject F)ᵒᵖ).obj
                        (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                    (Opposite.op { obj := A, pt := a, isGalois := isGalois })))
            u :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj
              (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
                (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                  (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                  (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
              (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
                  (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F })) :
              (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)
                  (((const (PointedGaloisObject F)ᵒᵖ).obj
                        (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                    (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 })))
            v :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj
              (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
                (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                  (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                  (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
              (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }))) →
      ∃ (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))
⊢ ∀
    (xj :
      (fun (X : Type u₂) ↦ X)
        (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
          (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }))),
    Eq (α :=
        (fun (X : Type u₂) ↦ X)
          (Functor.obj
            (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
              (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
            (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
                  (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })) :
              (a_1 :
                  (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)
                  (((const (PointedGaloisObject F)ᵒᵖ).obj
                        (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                    (Opposite.op { obj := A, pt := a, isGalois := isGalois })))
            u :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj
              (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
                (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                  (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                  (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
              (Opposite.op { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
                  (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F })) :
              (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)
                  (((const (PointedGaloisObject F)ᵒᵖ).obj
                        (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                    (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 })))
            xj :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj
              (Functor.obj (const (PointedGaloisObject F)ᵒᵖ)
                (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (F :=
                  (Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X)
                  (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))))
              (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }))) →
      ∃ (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))
              xj :
            (fun (X : Type u₂) ↦ X)
              (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) k))

Tactic:
(v : (B : C) ⟶ X)