awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
A : PointedGaloisObject F
⊢ Hom.val (𝟙 A) = 𝟙 A.obj

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C_1 : Type u₁
inst : Category.{u₂, u₁} C_1
inst_1 : GaloisCategory.{u₁, u₂} C_1
F : Functor.{u₂, w, u₁, w + 1} C_1 FintypeCat
A B C : PointedGaloisObject F
f : A ⟶ B
g : B ⟶ C
⊢ (f ≫ g).val = f.val ≫ g.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
A : PointedGaloisObject F
⊢ Functor.obj (incl F) A = A.obj

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
⊢ map (incl F) f = f.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat
A : PointedGaloisObject F
B : C
⊢ Eq (α :=
    (Functor.obj (Functor.op (incl F) ⋙ coyoneda) (Opposite.op A)).obj B ⟶
      (Functor.obj
            (Functor.obj (const (PointedGaloisObject F)ᵒᵖ) (Cocone.pt (J := (PointedGaloisObject F)ᵒᵖ) (cocone F)))
            (Opposite.op A)).obj
        B)
    (NatTrans.app (NatTrans.app (Cocone.ι (cocone F)) (Opposite.op A)) B)
    (↾fun (f : A.obj ⟶ 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 A.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
        A.pt)

Tactic:
rfl

Premises used: rfl
-- 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
obtain :
  ∀ (Z : C) (f : Z ⟶ Limits.prod.{u₂, u₁} A B) (z : (F.obj Z).obj) (hgal : IsGalois.{u₁, u₂} Z)
    (hfz :
      Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A 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 (A ⨯ B)))
            z :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A B)))
        (((Equiv.symm (fiberBinaryProductEquiv F A B) :
                (F.obj A).obj × (F.obj B).obj ≃ (F.obj (Limits.prod.{u₂, u₁} A B)).obj) :
              (a : (F.obj A).obj × (F.obj B).obj) → (F.obj (A ⨯ B)).obj)
            (a, b) :
          (F.obj (Limits.prod.{u₂, u₁} A B)).obj)),
    ∃ (W : PointedGaloisObject F) (x : W ⟶ { obj := A, pt := a, isGalois := isGalois }) (x :
      W ⟶ { obj := B, pt := b, isGalois := isGalois_1 }), True
⊢ ∃ (W : PointedGaloisObject F) (x : W ⟶ { obj := A, pt := a, isGalois := isGalois }) (x :
    W ⟶ { obj := B, pt := b, isGalois := isGalois_1 }), True

Tactic:
obtain ⟨Z, f, z, hgal, hfz⟩ := exists_hom_from_galois_of_fiber F (A ⨯ B)
      <| (fiberBinaryProductEquiv F A B).symm (a, b)

Premises used: Prod.mk, CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.prod
-- 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
Z : C
f : Z ⟶ Limits.prod.{u₂, u₁} A B
z : (F.obj Z).obj
hgal : IsGalois.{u₁, u₂} Z
hfz :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A 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 (A ⨯ B)))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A B)))
    (((Equiv.symm (fiberBinaryProductEquiv F A B) :
            (F.obj A).obj × (F.obj B).obj ≃ (F.obj (Limits.prod.{u₂, u₁} A B)).obj) :
          (a : (F.obj A).obj × (F.obj B).obj) → (F.obj (A ⨯ B)).obj)
        (a, b) :
      (F.obj (Limits.prod.{u₂, u₁} A B)).obj)
⊢ ∃ (W : PointedGaloisObject F) (x : W ⟶ { obj := A, pt := a, isGalois := isGalois }) (x :
    W ⟶ { obj := B, pt := b, isGalois := isGalois_1 }), True

Tactic:
⟨⟨Z, z, hgal⟩, ⟨f ≫ prod.fst, ?_⟩, ⟨f ≫ prod.snd, ?_⟩, trivial⟩

Premises used: trivial, CategoryTheory.Limits.prod.fst, CategoryTheory.Limits.prod.snd, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk, CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.mk
-- 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
Z : C
f : Z ⟶ Limits.prod.{u₂, u₁} A B
z : (F.obj Z).obj
hgal : IsGalois.{u₁, u₂} Z
hfz :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A 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 (A ⨯ B)))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A B)))
    (((Equiv.symm (fiberBinaryProductEquiv F A B) :
            (F.obj A).obj × (F.obj B).obj ≃ (F.obj (Limits.prod.{u₂, u₁} A B)).obj) :
          (a : (F.obj A).obj × (F.obj B).obj) → (F.obj (A ⨯ B)).obj)
        (a, b) :
      (F.obj (Limits.prod.{u₂, u₁} A B)).obj)
⊢ (@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 ≫ prod.fst)) :
        (a_1 :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj { obj := Z, pt := z, isGalois := hgal }.obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj { obj := A, pt := a, isGalois := isGalois }.obj))
      { obj := Z, pt := z, isGalois := hgal : PointedGaloisObject F }.pt =
    { obj := A, pt := a, isGalois := isGalois : PointedGaloisObject F }.pt

Tactic:
simp only [F.map_comp, hfz, FintypeCat.comp_apply, fiberBinaryProductEquiv_symm_fst_apply]

Premises used: FintypeCat.comp_apply, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply, CategoryTheory.Functor.map_comp
-- 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
Z : C
f : Z ⟶ Limits.prod.{u₂, u₁} A B
z : (F.obj Z).obj
hgal : IsGalois.{u₁, u₂} Z
hfz :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A 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 (A ⨯ B)))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (Limits.prod.{u₂, u₁} A B)))
    (((Equiv.symm (fiberBinaryProductEquiv F A B) :
            (F.obj A).obj × (F.obj B).obj ≃ (F.obj (Limits.prod.{u₂, u₁} A B)).obj) :
          (a : (F.obj A).obj × (F.obj B).obj) → (F.obj (A ⨯ B)).obj)
        (a, b) :
      (F.obj (Limits.prod.{u₂, u₁} A B)).obj)
⊢ (@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 ≫ prod.snd)) :
        (a :
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (F.obj { obj := Z, pt := z, isGalois := hgal }.obj)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (F.obj { obj := B, pt := b, isGalois := isGalois_1 }.obj))
      { obj := Z, pt := z, isGalois := hgal : PointedGaloisObject F }.pt =
    { obj := B, pt := b, isGalois := isGalois_1 : PointedGaloisObject F }.pt

Tactic:
simp only [F.map_comp, hfz, FintypeCat.comp_apply, fiberBinaryProductEquiv_symm_snd_apply]

Premises used: FintypeCat.comp_apply, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply, CategoryTheory.Functor.map_comp
-- 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
refine :
  (X : C) →
    IsColimit (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))
⊢ IsColimit (J := (PointedGaloisObject F)ᵒᵖ) (cocone F)

Tactic:
refine evaluationJointlyReflectsColimits _ (fun X ↦ ?_)

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsColimits
-- 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 : C
x : (F.obj X).obj
refine_1 :
  ∀ (Y : C) (i : Y ⟶ X) (y : (F.obj Y).obj)
    (h1 :
      (@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 i) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          y =
        x),
    IsConnected.{u₁, u₂} Y →
      Mono i →
        ∃ (i : (PointedGaloisObject F)ᵒᵖ) (xi :
          (fun (X : Type u₂) ↦ X)
            (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) i)),
          x =
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))) i) :
                (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i)) →
                  (fun (X : Type u₂) ↦ X)
                    (((const (PointedGaloisObject F)ᵒᵖ).obj
                          (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                      i))
              xi
⊢ ∃ (i : (PointedGaloisObject F)ᵒᵖ) (xi :
    (fun (X : Type u₂) ↦ X)
      (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) i)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))) i) :
          (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i)) →
            (fun (X : Type u₂) ↦ X)
              (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                i))
        xi

Tactic:
obtain ⟨Y, i, y, h1, _, _⟩ := fiber_in_connected_component F X x

Premises used: CategoryTheory.PreGaloisCategory.fiber_in_connected_component
-- 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 : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 :
  (@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 i) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      y =
    x
left : IsConnected.{u₁, u₂} Y
right : Mono i
refine_1 :
  ∀ (Z : C) (f : Z ⟶ Y) (z : (F.obj Z).obj) (hgal : IsGalois.{u₁, u₂} Z)
    (hfz :
      (@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 Y))
          z =
        y),
    ∃ (i : (PointedGaloisObject F)ᵒᵖ) (xi :
      (fun (X : Type u₂) ↦ X)
        (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))) i) :
            (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i)) →
              (fun (X : Type u₂) ↦ X)
                (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                  i))
          xi
⊢ ∃ (i : (PointedGaloisObject F)ᵒᵖ) (xi :
    (fun (X : Type u₂) ↦ X)
      (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) i)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))) i) :
          (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i)) →
            (fun (X : Type u₂) ↦ X)
              (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                i))
        xi

Tactic:
obtain ⟨Z, f, z, hgal, hfz⟩ := exists_hom_from_galois_of_fiber F Y y

Premises used: CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber
-- 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 : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 :
  (@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 i) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      y =
    x
left : IsConnected.{u₁, u₂} Y
right : Mono i
Z : C
f : Z ⟶ Y
z : (F.obj Z).obj
hgal : IsGalois.{u₁, u₂} Z
hfz :
  (@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 Y))
      z =
    y
⊢ ∃ (i : (PointedGaloisObject F)ᵒᵖ) (xi :
    (fun (X : Type u₂) ↦ X)
      (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) i)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))) i) :
          (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i)) →
            (fun (X : Type u₂) ↦ X)
              (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                i))
        xi

Tactic:
⟨⟨Z, z, hgal⟩, f ≫ i, ?_⟩

Premises used: Opposite.op, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk
-- 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 : C
x : (F.obj X).obj
Y : C
i : Y ⟶ X
y : (F.obj Y).obj
h1 :
  (@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 i) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      y =
    x
left : IsConnected.{u₁, u₂} Y
right : Mono i
Z : C
f : Z ⟶ Y
z : (F.obj Z).obj
hgal : IsGalois.{u₁, u₂} Z
hfz :
  (@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 Y))
      z =
    y
refine_1 :
  x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F)))
            (Opposite.op { obj := Z, pt := z, isGalois := hgal : PointedGaloisObject F })) :
        (a :
            (fun (X : Type u₂) ↦ X)
              ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj
                (Opposite.op { obj := Z, pt := z, isGalois := hgal }))) →
          (fun (X : Type u₂) ↦ X)
            (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
              (Opposite.op { obj := Z, pt := z, isGalois := hgal })))
      (f ≫ i)
⊢ ∃ (i : (PointedGaloisObject F)ᵒᵖ) (xi :
    (fun (X : Type u₂) ↦ X)
      (Functor.obj ((Functor.op (incl F) ⋙ coyoneda) ⋙ Functor.obj (evaluation C (Type u₂)) X) i)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (mapCocone (Functor.obj (evaluation C (Type u₂)) X) (cocone F))) i) :
          (a : (fun (X : Type u₂) ↦ X) ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).obj i)) →
            (fun (X : Type u₂) ↦ X)
              (((const (PointedGaloisObject F)ᵒᵖ).obj (((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).pt).obj
                i))
        xi

Tactic:
refine ⟨⟨Z, z, hgal⟩, f ≫ i, ?_⟩