awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat
inst_2 : FiberFunctor F
f g : End F
⊢ (endEquivAutGalois F : (a : End F) → AutGalois F) (g ≫ f) =
    HMul.hMul (α := AutGalois F) (β := AutGalois F) ((endEquivAutGalois F : (a : End F) → AutGalois F) g : AutGalois F)
      ((endEquivAutGalois F : (a : End F) → AutGalois F) f : AutGalois F)
have refine : ∀ (A : PointedGaloisObject F),
  Eq.{u₂ + 1} (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
    ((fun (f : Aut 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))
                _ _ _ (F.map f.hom) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
            A.pt :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)))
      ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj) ((endEquivAutGalois F : (a : End F) → AutGalois F) (g ≫ f))))
    ((fun (f : Aut 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))
                _ _ _ (F.map f.hom) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj))
            A.pt :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A.obj)))
      ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj)
        (HMul.hMul (α := AutGalois F) (β := AutGalois F)
          ((endEquivAutGalois F : (a : End F) → AutGalois F) g : AutGalois F)
          ((endEquivAutGalois F : (a : End F) → AutGalois F) f : AutGalois F))))
Tactic: refine AutGalois.ext F (fun A ↦ evaluation_aut_injective_of_isConnected F A A.pt ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : C ⥤ FintypeCat
inst_2 : FiberFunctor F
f : End F
⊢ IsIso f
have rw : IsUnit f
Tactic: rw [← isUnit_iff_isIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
⊢ (fun (t : (AutGalois F)ᵐᵒᵖ) ↦
        (asIso ((MulEquiv.symm (endMulEquivAutGalois F) : (a : (AutGalois F)ᵐᵒᵖ) → End F) t) : F ≅ F))
      ((MonoidHom.comp (↑(endMulEquivAutGalois F) : End F →* (AutGalois F)ᵐᵒᵖ) (Aut.toEnd F) :
          (a : Aut F) → (AutGalois F)ᵐᵒᵖ)
        t) =
    t
have simp : asIso ((Aut.toEnd F : (a : Aut F) → End F) t) = t
Tactic: simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
      MulEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
have refine : ∀ (x y : (F.obj X).obj), ∃ (g : Aut F), g • x = y
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
⊢ ∃ (g : Aut F), g • x = y
have obtain : ∀ (φ : Aut X) (h : φ • x = y), ∃ (g : Aut F), g • x = y
Tactic: obtain ⟨(φ : Aut X), h⟩ := MulAction.IsPretransitive.exists_smul_eq (M := Aut X) x y
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
⊢ ∃ (g : Aut F), g • x = y
have obtain : ∀ (a : AutGalois F)
  (ha :
    (AutGalois.π F { obj := X, pt := x, isGalois := sorry } :
          (a : AutGalois F) → Aut { obj := X, pt := x, isGalois := sorry }.obj)
        a =
      φ),
  ∃ (g : Aut F), g • x = y
Tactic: obtain ⟨a, ha⟩ := AutGalois.π_surjective F ⟨X, x, inferInstance⟩ φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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 =
    φ
⊢ ∃ (g : Aut F), g • x = y
have h₁ : HSMul.hSMul (α := Aut F)
    ((MulEquiv.symm (autMulEquivAutGalois F) : (a : (AutGalois F)ᵐᵒᵖ) → Aut F)
        { unop' := a : PreOpposite (AutGalois F) } :
      Aut F)
    x =
  y
Tactic: use (autMulEquivAutGalois F).symm ⟨a⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj
have obtain : ∀ (A : C) (f : A ⟶ X) (hgal : IsGalois.{u₁, u₂} A), MulAction.IsPretransitive (Aut F) (F.obj X).obj
Tactic: obtain ⟨A, f, hgal⟩ := exists_hom_from_galois_of_connected F X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (hypothesis)
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
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj
have 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))
Tactic: have hs : Function.Surjective (F.map f) := surjective_of_nonempty_fiber_of_isConnected F f
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
have refine : ∀ (x y : (F.obj X).obj), ∃ (g : Aut F), g • x = y
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
⊢ ∃ (g : Aut F), g • x = y
have 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
Tactic: obtain ⟨a, ha⟩ := hs x
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
⊢ ∃ (g : Aut F), g • x = y
have 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
Tactic: obtain ⟨b, hb⟩ := hs y
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (hypothesis)
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
⊢ ∃ (g : Aut F), g • x = y
have this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
Tactic: have : MulAction.IsPretransitive (Aut F) (F.obj A) := isPretransitive_of_isGalois F A
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
⊢ ∃ (g : Aut F), g • x = y
have obtain : ∀ (σ : Aut F)
  (hσ :
    (@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))
            _ _ _ (σ.hom.app A) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
        a =
      b),
  ∃ (g : Aut F), g • x = y
Tactic: obtain ⟨σ, (hσ : σ.hom.app A a = b)⟩ := MulAction.exists_smul_eq (Aut F) a b
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (goal)
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
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ :
  (@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))
          _ _ _ (σ.hom.app A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    b
⊢ ∃ (g : Aut F), g • x = y
have h : σ • x = y
Tactic: use σ
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
⊢ ∃ (g : Aut F), g • x = y
have hx' : let x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x;
x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
Tactic: set x' : F'.obj X := (e X).symm x with hx'
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Prorepresentability (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
hx' : x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
⊢ ∃ (g : Aut F), g • x = y
have hy' : let y' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y;
y' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
Tactic: set y' : F'.obj X := (e X).symm y with hy'