awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
⊢ g = 1
have h₁ : ∀ (X : C) (x : (F.obj X).obj),
  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))
            _ _ _ (g.hom.app X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (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))
            _ _ _ (NatTrans.app (Iso.hom 1) X : F.obj X ⟶ F.obj X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.IsFundamentalgroup (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
inst_4 : FiberFunctor F
inst_5 : TopologicalSpace G
inst_6 : IsTopologicalGroup G
inst_7 : CompactSpace G
inst_8 : IsFundamentalGroup F G
⊢ IsHomeomorph (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F)
have rw : Continuous (X := G) (Y := Aut F) (⇑(toAut F G) : (a : G) → Aut F) ∧
  Function.Bijective (α := G) (β := Aut F) (⇑(toAut F G) : (a : G) → Aut F)
Tactic: rw [isHomeomorph_iff_continuous_bijective]
-- 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 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
⊢ ∃ (W : PointedGaloisObject F) (x : W ⟶ { obj := A, pt := a, isGalois := isGalois }) (x :
    W ⟶ { obj := B, pt := b, isGalois := isGalois_1 }), True
have 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
Tactic: obtain ⟨Z, f, z, hgal, hfz⟩ := exists_hom_from_galois_of_fiber F (A ⨯ B)
      <| (fiberBinaryProductEquiv F A B).symm (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 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
have refine_1 : (@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: refine ⟨⟨Z, z, hgal⟩, ⟨f ≫ prod.fst, ?_⟩, ⟨f ≫ prod.snd, ?_⟩, trivial⟩
-- 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
⊢ IsColimit (J := (PointedGaloisObject F)ᵒᵖ) (cocone F)
have 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))
Tactic: refine evaluationJointlyReflectsColimits _ (fun 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
⊢ 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))
have refine_1 : ∀
  (x :
    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))),
  ∃ (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 Types.FilteredColimit.isColimitOf _ _ ?_ ?_
-- 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
x : (F.obj X).obj
⊢ ∃ (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
have 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
Tactic: obtain ⟨Y, i, y, h1, _, _⟩ := fiber_in_connected_component F X 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
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨Z, f, z, hgal, hfz⟩ := exists_hom_from_galois_of_fiber F Y 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
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
have 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)
Tactic: refine ⟨⟨Z, z, hgal⟩, f ≫ i, ?_⟩
-- 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
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
⊢ ∃ (a : (↑(Functor.obj (autGaloisSystem F) A) : Type u₂)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier)
            (X := Functor.obj (autGaloisSystem F) A) (map (autGaloisSystem F) f) :
          (a : (↑((autGaloisSystem F).obj A) : Type u₂)) → (↑((autGaloisSystem F).obj B) : Type u₂))
        a =
      φ
have obtain : ∀ (ψ : Aut A.obj) (hψ : autMap f.val ψ = φ),
  ∃ (a : (↑(Functor.obj (autGaloisSystem F) A) : Type u₂)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier)
            (X := Functor.obj (autGaloisSystem F) A) (map (autGaloisSystem F) f) :
          (a : (↑((autGaloisSystem F).obj A) : Type u₂)) → (↑((autGaloisSystem F).obj B) : Type u₂))
        a =
      φ
Tactic: obtain ⟨ψ, hψ⟩ := autMap_surjective_of_isGalois f.val φ
-- 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
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ ∃ (a : (↑(Functor.obj (autGaloisSystem F) A) : Type u₂)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier)
            (X := Functor.obj (autGaloisSystem F) A) (map (autGaloisSystem F) f) :
          (a : (↑((autGaloisSystem F).obj A) : Type u₂)) → (↑((autGaloisSystem F).obj B) : Type u₂))
        a =
      φ
have h : (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier)
        (X := Functor.obj (autGaloisSystem F) A) (map (autGaloisSystem F) f) :
      (a : (↑((autGaloisSystem F).obj A) : Type u₂)) → (↑((autGaloisSystem F).obj B) : Type u₂))
    ψ =
  φ
Tactic: use ψ
-- 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
f g : AutGalois F
h :
  ∀ (A : PointedGaloisObject F),
    Eq.{u₂ + 1} (α := Aut A.obj) ((π F A : (a : AutGalois F) → Aut A.obj) f : Aut A.obj)
      ((π F A : (a : AutGalois F) → Aut A.obj) g : Aut A.obj)
⊢ f = g
have a : ∀ (A : PointedGaloisObject F),
  (↑f : (j : PointedGaloisObject F) → (autGaloisSystem F ⋙ forget GrpCat).obj j) A =
    (↑g : (j : PointedGaloisObject F) → (autGaloisSystem F ⋙ forget GrpCat).obj j) A
Tactic: ext A
-- 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
A : PointedGaloisObject F
σ : Aut A.obj
⊢ ∃ (a : AutGalois F), (π F A : (a : AutGalois F) → Aut A.obj) a = σ
have this : ∀ (i : PointedGaloisObject F),
  Finite.{u₂ + 1}
    (Functor.obj
      (autGaloisSystem F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier))
      i)
Tactic: have (i : PointedGaloisObject F) : Finite ((autGaloisSystem F ⋙ forget _).obj i) :=
    inferInstanceAs <| Finite (Aut (i.obj))
-- 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 Y : PointedGaloisObject F
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj
        (autGaloisSystem F ⋙
          forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier))
        X ⟶
      Functor.obj (incl F ⋙ F ⋙ FintypeCat.incl) Y)
    (map
        (autGaloisSystem F ⋙
          forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier))
        f ≫
      Iso.hom ((fun (A : PointedGaloisObject F) ↦ (evaluationEquivOfIsGalois F A.obj A.pt).toIso) Y))
    (Iso.hom ((fun (A : PointedGaloisObject F) ↦ (evaluationEquivOfIsGalois F A.obj A.pt).toIso) X) ≫
      map (incl F ⋙ F ⋙ FintypeCat.incl) f)
have h : ∀
  (x :
    Functor.obj
      (autGaloisSystem F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier))
      X),
  Eq (α := Functor.obj (incl F ⋙ F ⋙ FintypeCat.incl) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map
            (autGaloisSystem F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC :=
                GrpCat.carrier))
            f ≫
          Iso.hom ((fun (A : PointedGaloisObject F) ↦ (evaluationEquivOfIsGalois F A.obj A.pt).toIso) Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom ((fun (A : PointedGaloisObject F) ↦ (evaluationEquivOfIsGalois F A.obj A.pt).toIso) X) ≫
          map (incl F ⋙ F ⋙ FintypeCat.incl) f))
      x)
Tactic: ext