awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (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
-- 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 rw : IsGalois.{u₁, u₂} X
⊢ MulAction.IsPretransitive.{u₂, w} (Aut X) (F.obj X).obj

Tactic:
rw [← isGalois_iff_pretransitive]

Premises used: CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive
-- 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 : IsGalois.{u₁, u₂} X
⊢ IsGalois.{u₁, u₂} X

Tactic:
infer_instance
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
change : g • n • g⁻¹ • x = x
⊢ (g * n * g⁻¹) • x = x

Tactic:
change g • n • (g⁻¹ • x) = x

Premises used: Inv.inv, HSMul.hSMul
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
⊢ ∃ (φ : Aut 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 φ.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x =
      g⁻¹ • x

Tactic:
have : ∃ (φ : Aut X), F.map φ.hom x = g⁻¹ • x :=
      MulAction.IsPretransitive.exists_smul_eq x (g⁻¹ • x)
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
this :
  ∃ (φ : Aut 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 φ.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x =
      g⁻¹ • x
obtain :
  ∀ (φ : Aut X)
    (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))
              _ _ _ (F.map φ.hom) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
          x =
        g⁻¹ • x),
    g • n • g⁻¹ • x = x
⊢ g • n • g⁻¹ • x = x

Tactic:
obtain ⟨φ, h⟩ := this
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
φ : Aut X
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))
          _ _ _ (F.map φ.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      x =
    g⁻¹ • x
rw : g • g⁻¹ • x = x
⊢ g • n • g⁻¹ • x = x

Tactic:
rw [← h, mulAction_naturality, ninstab, h]

Premises used: CategoryTheory.PreGaloisCategory.mulAction_naturality
-- 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 : IsGalois.{u₁, u₂} X
x : (F.obj X).obj
n : Aut F
ninstab : Membership.mem (γ := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) x) n
g : Aut F
φ : Aut X
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))
          _ _ _ (F.map φ.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      x =
    g⁻¹ • x
⊢ g • g⁻¹ • x = x

Tactic:
simp
-- 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
A : C
inst_3 : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
⊢ Function.Surjective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    fun (f : Aut A) ↦
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a

Tactic:
MulAction.IsPretransitive.exists_smul_eq a

Premises used: MulAction.IsPretransitive.exists_smul_eq, Function.Surjective
-- 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
A : C
inst_3 : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
⊢ Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    fun (f : Aut A) ↦
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a

Tactic:
⟨evaluation_aut_injective_of_isConnected F A a, evaluation_aut_surjective_of_isGalois F A a⟩

Premises used: And.intro, CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois, Function.Bijective, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected
-- 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
A : C
inst_3 : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
φ : Aut A
⊢ Eq.{w + 1} (α := (F.obj A).obj) ((evaluationEquivOfIsGalois F A a : (a : Aut A) → (F.obj A).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 φ.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))

Tactic:
rfl

Premises used: rfl
-- 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
A : C
inst_3 : IsGalois.{u₁, u₂} A
a b : (F.obj A).obj
change :
  (evaluationEquivOfIsGalois F A a : (a : Aut A) → (F.obj A).obj)
      (((evaluationEquivOfIsGalois F A a).symm : (a : (F.obj A).obj) → Aut A) b) =
    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 (Iso.hom (((evaluationEquivOfIsGalois F A a).symm : (a : (F.obj A).obj) → Aut A) b)) :
            F.obj A ⟶ F.obj A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    b

Tactic:
change (evaluationEquivOfIsGalois F A a) _ = _

Premises used: DFunLike.coe, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois
-- 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
A : C
inst_3 : IsGalois.{u₁, u₂} A
a b : (F.obj A).obj
⊢ (evaluationEquivOfIsGalois F A a : (a : Aut A) → (F.obj A).obj)
      (((evaluationEquivOfIsGalois F A a).symm : (a : (F.obj A).obj) → Aut A) b) =
    b

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
f : A ⟶ B
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
obtain : ∀ (a : (F.obj A).obj), ∃! τ : Aut B, f ≫ τ.hom = σ.hom ≫ f
⊢ ∃! τ : Aut B, f ≫ τ.hom = σ.hom ≫ f

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Premises used: CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
f : A ⟶ B
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∃! τ : Aut B, f ≫ τ.hom = σ.hom ≫ f

Tactic:
⟨?_, ?_, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
f : A ⟶ B
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Aut B

Tactic:
exact (evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, Equiv.symm, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut A
⊢ f ≫ (autMap f σ).hom = σ.hom ≫ f

Tactic:
(exists_autMap f σ).choose_spec.left

Premises used: Exists.choose_spec, CategoryTheory.PreGaloisCategory.exists_autMap, And.left
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut A
τ : Aut B
h : f ≫ τ.hom = σ.hom ≫ f
⊢ autMap f σ = τ

Tactic:
((exists_autMap f σ).choose_spec.right τ h).symm

Premises used: Exists.choose_spec, CategoryTheory.PreGaloisCategory.exists_autMap, And.right, CategoryTheory.PreGaloisCategory.autMap, Eq.symm
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A : C
inst_2 : IsGalois.{u₁, u₂} A
σ : Aut A
⊢ 𝟙 A ≫ (id σ).hom = σ.hom ≫ 𝟙 A

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X Y Z : C
inst_2 : IsConnected.{u₁, u₂} X
inst_3 : IsGalois.{u₁, u₂} Y
inst_4 : IsGalois.{u₁, u₂} Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ autMap (f ≫ g) = autMap g ∘ autMap f

Tactic:
funext fun σ ↦ autMap_unique _ σ _ ?_

Premises used: Function.comp, funext, CategoryTheory.PreGaloisCategory.autMap_unique, CategoryTheory.CategoryStruct.comp, CategoryTheory.PreGaloisCategory.autMap
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X Y Z : C
inst_2 : IsConnected.{u₁, u₂} X
inst_3 : IsGalois.{u₁, u₂} Y
inst_4 : IsGalois.{u₁, u₂} Z
f : X ⟶ Y
g : Y ⟶ Z
refine : ∀ (σ : Aut X), (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g
⊢ autMap (f ≫ g) = autMap g ∘ autMap f

Tactic:
refine funext fun σ ↦ autMap_unique _ σ _ ?_

Premises used: funext, CategoryTheory.PreGaloisCategory.autMap_unique
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X Y Z : C
inst_2 : IsConnected.{u₁, u₂} X
inst_3 : IsGalois.{u₁, u₂} Y
inst_4 : IsGalois.{u₁, u₂} Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
rw : (f ≫ (autMap f σ).hom) ≫ g = σ.hom ≫ f ≫ g
⊢ (f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g

Tactic:
rw [Function.comp_apply, Category.assoc, comp_autMap, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.PreGaloisCategory.comp_autMap, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
X Y Z : C
inst_2 : IsConnected.{u₁, u₂} X
inst_3 : IsGalois.{u₁, u₂} Y
inst_4 : IsGalois.{u₁, u₂} Z
f : X ⟶ Y
g : Y ⟶ Z
σ : Aut X
⊢ (f ≫ (autMap f σ).hom) ≫ g = σ.hom ≫ f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
inst_2 : IsGalois.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
obtain : ∀ (a : (F.obj A).obj), ∃ (a : Aut A), autMap f a = σ
⊢ ∃ (a : Aut A), autMap f a = σ

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Premises used: CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
inst_2 : IsGalois.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
obtain :
  ∀ (a' : (F.obj A).obj)
    (ha' :
      Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            a' :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 σ.hom) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 A)) →
                    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
                a :
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))),
    ∃ (a : Aut A), autMap f a = σ
⊢ ∃ (a : Aut A), autMap f a = σ

Tactic:
obtain ⟨a', ha'⟩ := surjective_of_nonempty_fiber_of_isConnected F f (F.map σ.hom (F.map f a))

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
inst_2 : IsGalois.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).obj
ha' :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
        a' :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 σ.hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 A)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
            a :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B)) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj B))
τ : Aut A
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))
          _ _ _ (F.map τ.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    a'
h : autMap f τ = σ
⊢ ∃ (a : Aut A), autMap f a = σ

Tactic:
use τ
-- Module: Mathlib.CategoryTheory.Galois.GaloisObjects
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
A B : C
inst_2 : IsConnected.{u₁, u₂} A
inst_3 : IsGalois.{u₁, u₂} B
f : A ⟶ B
σ τ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
obtain : ∀ (a : (F.obj A).obj), autMap f (σ * τ) = autMap f σ * autMap f τ
⊢ autMap f (σ * τ) = autMap f σ * autMap f τ

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Premises used: CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
g : G
X : C
x : (F.obj X).obj
⊢ (fun (x : (F.obj X).obj) ↦ g⁻¹ • x) ((fun (x : (F.obj X).obj) ↦ g • x) x) = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : Type u_1
inst_1 : Group G
inst_2 : (X : C) → MulAction.{u_1, w} G (F.obj X).obj
g : G
X : C
x : (F.obj X).obj
⊢ (fun (x : (F.obj X).obj) ↦ g • x) ((fun (x : (F.obj X).obj) ↦ g⁻¹ • x) x) = x

Tactic:
simp