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 : C ⥤ FintypeCat
inst_2 : FiberFunctor F
t : Aut F
⊢ asIso ((Aut.toEnd F : (a : Aut F) → End F) t) = t

Tactic:
exact Aut.ext rfl

Premises used: CategoryTheory.Aut.ext, 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
t : (AutGalois F)ᵐᵒᵖ
⊢ (endMulEquivAutGalois F : (a : End F) → (AutGalois F)ᵐᵒᵖ)
      (↑((MulEquiv.symm (Aut.unitsEndEquivAut F) : (a : Aut F) → (End F)ˣ)
            (asIso ((MulEquiv.symm (endMulEquivAutGalois F) : (a : (AutGalois F)ᵐᵒᵖ) → End F) t))) :
        End F) =
    t

Tactic:
(MulEquiv.eq_symm_apply (endMulEquivAutGalois F)).mp rfl

Premises used: MulEquiv.eq_symm_apply, Iff.mp, rfl, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois
-- 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
t : (AutGalois F)ᵐᵒᵖ
⊢ (endMulEquivAutGalois F : (a : End F) → (AutGalois F)ᵐᵒᵖ)
      (↑((MulEquiv.symm (Aut.unitsEndEquivAut F) : (a : Aut F) → (End F)ˣ)
            (asIso ((MulEquiv.symm (endMulEquivAutGalois F) : (a : (AutGalois F)ᵐᵒᵖ) → End F) t))) :
        End F) =
    t

Tactic:
exact (MulEquiv.eq_symm_apply (endMulEquivAutGalois F)).mp rfl

Premises used: MulEquiv.eq_symm_apply, Iff.mp, rfl, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois
-- 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 y : Aut F),
    (MonoidHom.comp (↑(endMulEquivAutGalois F) : End F →* (AutGalois F)ᵐᵒᵖ) (Aut.toEnd F) :
          (a : Aut F) → (AutGalois F)ᵐᵒᵖ)
        (x * y) =
      HMul.hMul (α := (AutGalois F)ᵐᵒᵖ) (β := (AutGalois F)ᵐᵒᵖ)
        ((MonoidHom.comp (↑(endMulEquivAutGalois F) : End F →* (AutGalois F)ᵐᵒᵖ) (Aut.toEnd F) :
              (a : Aut F) → (AutGalois F)ᵐᵒᵖ)
            x :
          (AutGalois F)ᵐᵒᵖ)
        ((MonoidHom.comp (↑(endMulEquivAutGalois F) : End F →* (AutGalois F)ᵐᵒᵖ) (Aut.toEnd F) :
              (a : Aut F) → (AutGalois F)ᵐᵒᵖ)
            y :
          (AutGalois F)ᵐᵒᵖ)

Tactic:
simp [map_mul]

Premises used: map_mul
-- 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
f : Aut F
A : C
inst_3 : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
⊢ Eq (α := (F.obj A).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))
            _ _ _
            (NatTrans.app (↑((MulEquiv.symm (Aut.unitsEndEquivAut F) : (a : Aut F) → (End F)ˣ) f) : End F)
                { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.obj :
              F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.obj ⟶
                F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.obj) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj))
        { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.pt :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.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.hom.app A) :
          (a : (F.obj A).obj) → (F.obj A).obj)
        a :
      (F.obj A).obj)

Tactic:
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 : AutGalois F
A : C
inst_3 : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    ((@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
                (Iso.hom
                  ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F } :
                      (a_1 : AutGalois F) → Aut { obj := A, pt := a, isGalois := ⋯ }.obj)
                    (MulOpposite.unop { unop' := x }))) :
              F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.obj ⟶
                F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.obj) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }.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
                (Iso.hom
                  ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ } :
                      (a_1 : AutGalois F) → Aut { obj := A, pt := a, isGalois := ⋯ }.obj)
                    x)) :
              F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ : PointedGaloisObject F }) ⟶
                F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ })) :
          (a_1 :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj { obj := A, pt := a, isGalois := ⋯ }.obj))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (F.obj (PointedGaloisObject.obj { obj := A, pt := a, isGalois := ⋯ })))

Tactic:
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 : C
inst_3 : IsGalois.{u₁, u₂} X
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: MulAction.IsPretransitive.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
inst_3 : IsGalois.{u₁, u₂} X
refine : ∀ (x y : (F.obj X).obj), ∃ (g : Aut F), g • x = y
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- 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
inst_3 : IsGalois.{u₁, u₂} X
x y : (F.obj X).obj
obtain : ∀ (φ : Aut X) (h : φ • x = y), ∃ (g : Aut F), g • x = y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
obtain ⟨(φ : Aut X), h⟩ := MulAction.IsPretransitive.exists_smul_eq (M := Aut X) x y

Premises used: MulAction.IsPretransitive.exists_smul_eq, CategoryTheory.Aut
-- 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
inst_3 : IsGalois.{u₁, u₂} X
x y : (F.obj X).obj
φ : Aut X
h : φ • x = y
obtain :
  ∀ (a : AutGalois F)
    (ha :
      (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ } :
            (a : AutGalois F) → Aut { obj := X, pt := x, isGalois := ⋯ }.obj)
          a =
        φ),
    ∃ (g : Aut F), g • x = y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
obtain ⟨a, ha⟩ := AutGalois.π_surjective F ⟨X, x, inferInstance⟩ φ

Premises used: inferInstance, CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk, CategoryTheory.PreGaloisCategory.AutGalois.π_surjective
-- 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
inst_3 : IsGalois.{u₁, u₂} X
x y : (F.obj X).obj
φ : Aut X
h : φ • x = y
a : AutGalois F
ha :
  (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ } :
        (a : AutGalois F) → Aut { obj := X, pt := x, isGalois := ⋯ }.obj)
      a =
    φ
h₁ :
  HSMul.hSMul (α := Aut F)
      ((MulEquiv.symm (autMulEquivAutGalois F) : (a : (AutGalois F)ᵐᵒᵖ) → Aut F)
          { unop' := a : PreOpposite (AutGalois F) } :
        Aut F)
      x =
    y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
use (autMulEquivAutGalois F).symm ⟨a⟩

Premises used: CategoryTheory.PreGaloisCategory.autMulEquivAutGalois, PreOpposite.op', MulEquiv.symm, DFunLike.coe
-- 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
inst_3 : IsGalois.{u₁, u₂} X
x y : (F.obj X).obj
φ : Aut X
h : φ • x = y
a : AutGalois F
ha :
  (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ } :
        (a : AutGalois F) → Aut { obj := X, pt := x, isGalois := ⋯ }.obj)
      a =
    φ
⊢ HSMul.hSMul (α := Aut F)
      ((MulEquiv.symm (autMulEquivAutGalois F) : (a : (AutGalois F)ᵐᵒᵖ) → Aut F)
          { unop' := a : PreOpposite (AutGalois F) } :
        Aut F)
      x =
    y

Tactic:
simpa [mulAction_def, ha]

Premises used: CategoryTheory.PreGaloisCategory.mulAction_def
-- 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
inst_3 : IsConnected.{u₁, u₂} X
obtain : ∀ (A : C) (f : A ⟶ X) (hgal : IsGalois.{u₁, u₂} A), MulAction.IsPretransitive (Aut F) (F.obj X).obj
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
obtain ⟨A, f, hgal⟩ := exists_hom_from_galois_of_connected F X

Premises used: CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_connected
-- 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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
⊢ Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))

Tactic:
have hs : Function.Surjective (F.map f) := surjective_of_nonempty_fiber_of_isConnected F f
-- 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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
hs :
  Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: MulAction.IsPretransitive.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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
hs :
  Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
refine : ∀ (x y : (F.obj X).obj), ∃ (g : Aut F), g • x = y
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- 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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
hs :
  Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
x y : (F.obj X).obj
obtain :
  ∀ (a : (F.obj A).obj)
    (ha :
      (@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 =
        x),
    ∃ (g : Aut F), g • x = y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
obtain ⟨a, ha⟩ := hs x
-- 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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
hs :
  Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
x y : (F.obj X).obj
a : (F.obj A).obj
ha :
  (@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 =
    x
obtain :
  ∀ (b : (F.obj A).obj)
    (hb :
      (@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))
          b =
        y),
    ∃ (g : Aut F), g • x = y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
obtain ⟨b, hb⟩ := hs y
-- 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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
hs :
  Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
x y : (F.obj X).obj
a : (F.obj A).obj
ha :
  (@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 =
    x
b : (F.obj A).obj
hb :
  (@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))
      b =
    y
⊢ MulAction.IsPretransitive (Aut F) (F.obj A).obj

Tactic:
have : MulAction.IsPretransitive (Aut F) (F.obj A) := isPretransitive_of_isGalois F A