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
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
⊢ 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:
simp [← hfz, ← h1]
-- 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
x : AutGalois F
⊢ (π F A : (a : AutGalois F) → Aut A.obj) x =
    (↑x : (j : PointedGaloisObject F) → (autGaloisSystem F ⋙ forget GrpCat).obj j) A

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 B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
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 =
        φ
⊢ ∃ (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 φ

Premises used: CategoryTheory.PreGaloisCategory.autMap_surjective_of_isGalois, CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.val
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
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 ψ = φ
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₂))
      ψ =
    φ
⊢ ∃ (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:
use ψ
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
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 ψ = φ
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier)
          (GrpCat.ofHom (autMapHom f.val)) :
        (a : (↑((autGaloisSystem F).obj A) : Type u₂)) → (↑((autGaloisSystem F).obj B) : Type u₂))
      ψ =
    φ

Tactic:
hψ

Premises used: Classical.choose, CategoryTheory.PreGaloisCategory.autMap, 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
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier)
          (GrpCat.ofHom (autMapHom f.val)) :
        (a : (↑((autGaloisSystem F).obj A) : Type u₂)) → (↑((autGaloisSystem F).obj B) : Type u₂))
      ψ =
    φ

Tactic:
exact hψ
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
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)
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
⊢ f = g

Tactic:
ext A
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
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)
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:
h A

Premises used: 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
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)
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:
exact h A
-- 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
A : PointedGaloisObject F
σ : Aut A.obj
⊢ ∀ (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))
-- 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
A : PointedGaloisObject F
σ : Aut A.obj
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)
⊢ ∃ (a : AutGalois F), (π F A : (a : AutGalois F) → Aut A.obj) a = σ

Tactic:
eval_section_surjective_of_surjective
    (autGaloisSystem F ⋙ forget _) (autGaloisSystem_map_surjective F) A σ

Premises used: CategoryTheory.Functor.comp, CategoryTheory.forget, CategoryTheory.PreGaloisCategory.AutGalois, CategoryTheory.Aut, CategoryTheory.PreGaloisCategory.autGaloisSystem, CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective, CategoryTheory.Functor.eval_section_surjective_of_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
A : PointedGaloisObject F
σ : Aut A.obj
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)
⊢ ∃ (a : AutGalois F), (π F A : (a : AutGalois F) → Aut A.obj) a = σ

Tactic:
exact eval_section_surjective_of_surjective
    (autGaloisSystem F ⋙ forget _) (autGaloisSystem_map_surjective F) A σ

Premises used: CategoryTheory.Functor.comp, CategoryTheory.forget, CategoryTheory.PreGaloisCategory.autGaloisSystem, CategoryTheory.PreGaloisCategory.autGaloisSystem_map_surjective, CategoryTheory.Functor.eval_section_surjective_of_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
f : End F
A : PointedGaloisObject F
⊢ Eq (α := (F.obj A.obj).obj)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              ((FullyFaithful.homEquiv ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C) :
                  (a : F ⟶ F) → F ⋙ FintypeCat.incl ⟶ F ⋙ FintypeCat.incl)
                f)
              A.obj) :
          (a : (F.obj A.obj).obj) → (F.obj A.obj).obj)
        A.pt :
      (F.obj A.obj).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.app A.obj : F.obj A.obj ⟶ F.obj A.obj) :
          (a : (F.obj A.obj).obj) → (F.obj A.obj).obj)
        A.pt :
      (F.obj A.obj).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 Y : PointedGaloisObject F
f : X ⟶ Y
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)
⊢ 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)

Tactic:
ext
-- 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 : PointedGaloisObject F
f : X ⟶ Y
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:
simp [evaluationEquivOfIsGalois, -Hom.comp, ← f.comp]

Premises used: CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois
-- 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
A : PointedGaloisObject F
b : (F.obj A.obj).obj
⊢ Eq (α :=
    (fun (X : Type u₂) ↦ X)
      (Functor.obj
        (autGaloisSystem F ⋙
          forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier))
        A))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.inv (autIsoFibers F)) A) :
          (a : (fun (X : Type u₂) ↦ X) ((incl F ⋙ F ⋙ FintypeCat.incl).obj A)) →
            (fun (X : Type u₂) ↦ X) ((autGaloisSystem F ⋙ forget GrpCat).obj A))
        b :
      (fun (X : Type u₂) ↦ X)
        (Functor.obj
          (autGaloisSystem F ⋙
            forget GrpCat (FC := fun (x1 x2 : GrpCat.{u₂}) ↦ (↑x1 : Type u₂) →* (↑x2 : Type u₂)) (CC := GrpCat.carrier))
          A))
    (((evaluationEquivOfIsGalois F A.obj A.pt).symm : (a : (F.obj A.obj).obj) → Aut A.obj) b : Aut 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 : 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)

Tactic:
AutGalois.ext F (fun A ↦ evaluation_aut_injective_of_isConnected F A A.pt ?_)

Premises used: CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt, CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj, CategoryTheory.PreGaloisCategory.AutGalois.ext, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
-- 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 g : End F
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))))
⊢ (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)

Tactic:
refine AutGalois.ext F (fun A ↦ evaluation_aut_injective_of_isConnected F A A.pt ?_)

Premises used: CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt, CategoryTheory.PreGaloisCategory.PointedGaloisObject.obj, CategoryTheory.PreGaloisCategory.AutGalois.ext, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
-- 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 : End F),
    Equiv.toFun (Equiv.trans (endEquivAutGalois F) MulOpposite.opEquiv) (x * y) =
      HMul.hMul (α := (AutGalois F)ᵐᵒᵖ) (Equiv.toFun (Equiv.trans (endEquivAutGalois F) MulOpposite.opEquiv) x)
        (Equiv.toFun (Equiv.trans (endEquivAutGalois F) MulOpposite.opEquiv) y)

Tactic:
simp
-- 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 : End F
A : PointedGaloisObject F
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (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))
            _ _ _
            (F.map
                (Iso.hom
                  ((AutGalois.π F A : (a : AutGalois F) → Aut A.obj)
                    (MulOpposite.unop ((endMulEquivAutGalois F : (a : End F) → (AutGalois F)ᵐᵒᵖ) f)))) :
              F.obj A.obj ⟶ F.obj A.obj) :
          (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))
    ((@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.app A.obj : F.obj A.obj ⟶ F.obj A.obj) :
          (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))

Tactic:
endEquivAutGalois_π F f A

Premises used: CategoryTheory.PreGaloisCategory.endEquivAutGalois_π
-- 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 : End F
⊢ IsUnit f

Tactic:
(isUnit_map_iff (endMulEquivAutGalois F) _).mp
    (Group.isUnit ((endMulEquivAutGalois F) f))

Premises used: Group.isUnit, isUnit_map_iff, Iff.mp, DFunLike.coe, 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
f : End F
rw : IsUnit f
⊢ IsIso f

Tactic:
rw [← isUnit_iff_isIso]

Premises used: CategoryTheory.isUnit_iff_isIso
-- 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 : End F
⊢ IsUnit f

Tactic:
FibreFunctor.end_isUnit F f

Premises used: CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit
-- 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 : End F
⊢ IsUnit f

Tactic:
exact FibreFunctor.end_isUnit F f

Premises used: CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit
-- 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
simp : asIso ((Aut.toEnd F : (a : Aut F) → End F) t) = t
⊢ (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

Tactic:
simp only [MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
      MulEquiv.symm_apply_apply]

Premises used: MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, MulEquiv.symm_apply_apply
-- 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:
Aut.ext rfl

Premises used: CategoryTheory.Aut.ext, rfl