awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this : IsIso (i ≫ (functorToAction F).map prod.fst)
⊢ IsIso (v.inv ≫ i ≫ (functorToAction F).map prod.fst)

Tactic:
apply IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso ((functorToAction F).map ψ)

Tactic:
have : IsIso ((functorToAction F).map ψ) := by
      simp only [map_comp, hgvi, Category.assoc, ψ]
      have : IsIso (i ≫ (functorToAction F).map prod.fst) := by
        suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
        infer_instance
      apply IsIso.comp_isIso
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this : IsIso ((functorToAction F).map ψ)
⊢ IsIso ψ

Tactic:
have : IsIso ψ := isIso_of_reflects_iso ψ (functorToAction F)
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this_2 : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
h : (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = f
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f

Tactic:
use inv ψ ≫ g ≫ prod.snd

Premises used: CategoryTheory.Limits.prod.snd, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this_2 : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
h : (functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = (functorToAction F).map ψ ≫ f
⊢ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = f

Tactic:
rw [← cancel_epi ((functorToAction F).map ψ)]

Premises used: CategoryTheory.Functor.map, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this_2 : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
h :
  ∀ (z : (F.obj Z).obj),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
      ((@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))
              _ _ _ ((functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd)).hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Z).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
          z :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
      ((@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))
              _ _ _ ((functorToAction F).map ψ ≫ f).hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Z).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
          z :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
⊢ (functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd) = (functorToAction F).map ψ ≫ f

Tactic:
ext (z : F.obj Z)

Premises used: CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this_2 : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
z : (F.obj Z).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
    ((@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))
            _ _ _ ((functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd)).hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Z).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
    ((@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))
            _ _ _ ((functorToAction F).map ψ ≫ f).hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Z).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj Y).V)

Tactic:
simp [-FintypeCat.comp_apply, -Action.comp_hom, i, u, ψ, hgvi]

Premises used: Action.comp_hom, FintypeCat.comp_apply
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
G : Type v
inst : Group G
inst_1 : Finite G
choose :
  ∀ (G' : Type) (hg : Group G') (hf : Fintype G') (e : Nonempty.{max 1 (v + 1)} (G ≃* G')),
    PreservesColimitsOfShape.{v, 0, w, w, w + 1, w + 1} (SingleObj G) FintypeCat.incl
⊢ PreservesColimitsOfShape.{v, 0, w, w, w + 1, w + 1} (SingleObj G) FintypeCat.incl

Tactic:
choose G' hg hf e using Finite.exists_type_univ_nonempty_mulEquiv G

Premises used: Finite.exists_type_univ_nonempty_mulEquiv
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
G : Type v
inst : Group G
inst_1 : Finite G
G' : Type
hg : Group G'
hf : Fintype G'
e : Nonempty.{max 1 (v + 1)} (G ≃* G')
⊢ PreservesColimitsOfShape.{v, 0, w, w, w + 1, w + 1} (SingleObj G) FintypeCat.incl

Tactic:
Limits.preservesColimitsOfShape_of_equiv (Classical.choice e).toSingleObjEquiv.symm _

Premises used: MulEquiv.toSingleObjEquiv, Classical.choice, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
G : Type v
inst : Group G
inst_1 : Finite G
G' : Type
hg : Group G'
hf : Fintype G'
e : Nonempty.{max 1 (v + 1)} (G ≃* G')
⊢ PreservesColimitsOfShape.{v, 0, w, w, w + 1, w + 1} (SingleObj G) FintypeCat.incl

Tactic:
exact Limits.preservesColimitsOfShape_of_equiv (Classical.choice e).toSingleObjEquiv.symm _

Premises used: MulEquiv.toSingleObjEquiv, Classical.choice, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
g h : Aut X
a : (F.obj X).obj
change :
  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))
            _ _ _ (F.map (h.hom ≫ g.hom)) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        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 h.hom ≫ F.map g.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ (g * h) • a = g • h • a

Tactic:
change F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
g h : Aut X
a : (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))
            _ _ _ (F.map (h.hom ≫ g.hom)) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        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 h.hom ≫ F.map g.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))

Tactic:
simp only [map_comp, FintypeCat.comp_apply]

Premises used: FintypeCat.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
a : (F.obj X).obj
change :
  (@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 (𝟙 X)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a =
    a
⊢ HSMul.hSMul.{u₂, w, w} (α := Aut X) 1 a = a

Tactic:
change F.map (𝟙 X) a = a

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
a : (F.obj X).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 (𝟙 X)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a =
    a

Tactic:
simp only [map_id, FintypeCat.id_apply]

Premises used: FintypeCat.id_apply, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
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
J : Functor.{u₂, u₂, 0, u₁} (SingleObj.{u₂} (Aut X)) C := SingleObj.functor (Aut.toEnd X)
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient.{u₂, w} (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) :=
  preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫ (SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl)).toIso
e₁ :
  IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))) ≃
    IsLimit
      (asEmptyCone
        (Quot (α := (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))
          (⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))) :
            (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) →
              (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) → Prop)))
e₂ :
  IsLimit
      (asEmptyCone
        (Quot (α := (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))
          (⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))) :
            (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) →
              (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) → Prop))) ≃
    Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)
β : Type (w + 1)
⊢ IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))) ≃
    Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)

Tactic:
apply Equiv.trans

Premises used: Equiv.trans
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
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
J : Functor.{u₂, u₂, 0, u₁} (SingleObj.{u₂} (Aut X)) C := SingleObj.functor (Aut.toEnd X)
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient.{u₂, w} (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) :=
  preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫ (SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl)).toIso
⊢ IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))) ≃
    IsLimit
      (asEmptyCone
        (Quot (α := (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))
          (⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))) :
            (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) →
              (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) → Prop)))

Tactic:
apply (IsTerminal.isTerminalIffObj (F ⋙ FintypeCat.incl) _).trans
      (isLimitEmptyConeEquiv _ (asEmptyCone _) (asEmptyCone _) e)

Premises used: CategoryTheory.Limits.IsTerminal.isTerminalIffObj, Equiv.trans, CategoryTheory.Functor.comp, CategoryTheory.Limits.isLimitEmptyConeEquiv, FintypeCat.incl, CategoryTheory.Limits.asEmptyCone
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
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
J : Functor.{u₂, u₂, 0, u₁} (SingleObj.{u₂} (Aut X)) C := SingleObj.functor (Aut.toEnd X)
e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅
  MulAction.orbitRel.Quotient.{u₂, w} (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X))) :=
  preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫ (SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl)).toIso
⊢ IsLimit
      (asEmptyCone
        (Quot (α := (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))
          (⇑(MulAction.orbitRel (Aut X) ((J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)))) :
            (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) →
              (J ⋙ F ⋙ FintypeCat.incl).obj (SingleObj.star (Aut X)) → Prop))) ≃
    Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)

Tactic:
exact Types.isTerminalEquivUnique _

Premises used: CategoryTheory.Limits.Types.isTerminalEquivUnique
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X : C
inst_2 : IsConnected.{u₁, u₂} X
⊢ IsGalois.{u₁, u₂} X ↔
    Nonempty
      (IsTerminal.{u₂, u₁} (colimit.{u₂, 0, u₂, u₁} (J := SingleObj.{u₂} (Aut X)) (SingleObj.functor (Aut.toEnd X))))

Tactic:
⟨fun h ↦ h.quotientByAutTerminal, fun h ↦ ⟨h⟩⟩

Premises used: CategoryTheory.PreGaloisCategory.IsGalois.mk, Iff.intro, CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
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
rw :
  Nonempty.{w + 1} (Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)) ↔
    MulAction.IsPretransitive.{u₂, w} (Aut X) (F.obj X).obj
⊢ IsGalois.{u₁, u₂} X ↔ MulAction.IsPretransitive.{u₂, w} (Aut X) (F.obj X).obj

Tactic:
rw [isGalois_iff_aux, Equiv.nonempty_congr <| quotientByAutTerminalEquivUniqueQuotient F X]

Premises used: CategoryTheory.PreGaloisCategory.isGalois_iff_aux, CategoryTheory.PreGaloisCategory.quotientByAutTerminalEquivUniqueQuotient, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
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
⊢ Nonempty.{w + 1} (Unique (MulAction.orbitRel.Quotient.{u₂, w} (Aut X) (F.obj X).obj)) ↔
    MulAction.IsPretransitive.{u₂, w} (Aut X) (F.obj X).obj

Tactic:
(MulAction.pretransitive_iff_unique_quotient_of_nonempty (Aut X) (F.obj X)).symm

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Aut, Iff.symm, MulAction.pretransitive_iff_unique_quotient_of_nonempty, CategoryTheory.Functor.obj