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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
hs :
  Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    (⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
x y : (F.obj X).obj
a : (F.obj A).obj
ha :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a =
    x
b : (F.obj A).obj
hb :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      b =
    y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
obtain :
  ∀ (σ : Aut F)
    (hσ :
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ (σ.hom.app A) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
          a =
        b),
    ∃ (g : Aut F), g • x = y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
obtain ⟨σ, (hσ : σ.hom.app A a = b)⟩ := MulAction.exists_smul_eq (Aut F) a b

Premises used: CategoryTheory.Aut, MulAction.exists_smul_eq
-- 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
inst_3 : IsConnected.{u₁, u₂} X
A : C
f : A ⟶ X
hgal : IsGalois.{u₁, u₂} A
hs :
  Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    (⇑(@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f)) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
x y : (F.obj X).obj
a : (F.obj A).obj
ha :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      a =
    x
b : (F.obj A).obj
hb :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      b =
    y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (σ.hom.app A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    b
h : σ • x = y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
use σ
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
⊢ let x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x;
  x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x

Tactic:
set x' : F'.obj X := (e X).symm x with hx'

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
hx' : x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
⊢ let y' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y;
  y' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y

Tactic:
set y' : F'.obj X := (e X).symm y with hy'

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
hx' : x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
y' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
hy' : y' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
obtain :
  ∀ (g' : Aut F')
    (hg' :
      (@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' =
        y'),
    ∃ (g : Aut F), g • x = y
⊢ ∃ (g : Aut F), g • x = y

Tactic:
obtain ⟨g', (hg' : g'.hom.app X x' = y')⟩ := MulAction.exists_smul_eq (Aut F') x' y'

Premises used: CategoryTheory.Aut, MulAction.exists_smul_eq
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
hx' : x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
y' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
hy' : y' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
g' : Aut F'
hg' :
  (@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' =
    y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun (Y : C) ↦
    (FintypeCat.equivEquivIso : (a : (F.obj Y).obj ≃ (F.obj Y).obj) → F.obj Y ≅ F.obj Y)
      ((e Y).symm.trans
        (Equiv.trans
          ((Equiv.symm FintypeCat.equivEquivIso : (a : F'.obj Y ≅ F'.obj Y) → (F'.obj Y).obj ≃ (F'.obj Y).obj)
            (Iso.app g' Y))
          (e Y)))
g : F ≅ F := NatIso.ofComponents gapp ⋯
⊢ ∃ (g : Aut F), g • x = y

Tactic:
⟨g, show (gapp X).hom x = y from ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.Prorepresentability
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : GaloisCategory.{u₁, u₂} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_2 : FiberFunctor F
X : C
inst_3 : IsConnected.{u₁, u₂} X
x y : (F.obj X).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
e : (Y : C) → Equiv.{u₂ + 1, w + 1} (F'.obj Y).obj (F.obj Y).obj := fun (Y : C) ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
hx' : x' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) x
y' : (F'.obj X).obj := ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
hy' : y' = ((e X).symm : (a : (F.obj X).obj) → (F'.obj X).obj) y
g' : Aut F'
hg' :
  (@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' =
    y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun (Y : C) ↦
    (FintypeCat.equivEquivIso : (a : (F.obj Y).obj ≃ (F.obj Y).obj) → F.obj Y ≅ F.obj Y)
      ((e Y).symm.trans
        (Equiv.trans
          ((Equiv.symm FintypeCat.equivEquivIso : (a : F'.obj Y ≅ F'.obj Y) → (F'.obj Y).obj ≃ (F'.obj Y).obj)
            (Iso.app g' Y))
          (e Y)))
g : F ≅ F := NatIso.ofComponents gapp ⋯
⊢ (@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))
          _ _ _ (gapp X).hom :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      x =
    y

Tactic:
simp [gapp, ← hx', hg', hy', Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
σ : Aut F
X : C
⊢ (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X = Iso.app σ X

Tactic:
rfl

Premises used: CategoryTheory.Iso.app, rfl
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
σ τ : Aut F
h :
  Eq (α := (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ : (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) τ : (X : C) → Aut (F.obj X))
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))
              _ _ _ (σ.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))
              _ _ _ (τ.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))
⊢ σ = τ

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
σ τ : Aut F
h :
  Eq (α := (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ : (X : C) → Aut (F.obj X))
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) τ : (X : C) → Aut (F.obj X))
X : C
x : (F.obj X).obj
⊢ Iso.app σ X = Iso.app τ X

Tactic:
have : σ.app X = τ.app X := congr_fun h X
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
⊢ DiscreteTopology.{w} (F.obj X).obj

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X Y : C
⊢ Eq (α := TopologicalSpace (F.obj X ⟶ F.obj Y)) (instTopologicalSpaceHomFintypeCatObj F) ⊥

Tactic:
simp [DiscreteTopology.eq_bot]

Premises used: DiscreteTopology.eq_bot
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X : C
⊢ DiscreteTopology.{w} (Aut (F.obj X))

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
h :
  ∀ (a : (X : C) → Aut (F.obj X)),
    Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
        (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X))) a ↔
      Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
        (⋂ (f : Arrow.{u₂, u₁} C),
          {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})
        a
⊢ Eq (α := Set ((X : C) → Aut (F.obj X)))
    (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)))
    (⋂ (f : Arrow.{u₂, u₁} C),
      {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})

Tactic:
ext a
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
h :
  (∃ (y : Aut F), (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) y = a) ↔
    ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom
⊢ Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
      (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X))) a ↔
    Membership.mem (γ := Set ((X : C) → Aut (F.obj X)))
      (⋂ (f : Arrow.{u₂, u₁} C),
        {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})
      a

Tactic:
simp +instances only [Set.mem_range, Set.mem_iInter, Set.mem_setOf_eq]

Premises used: Set.mem_range, Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
h :
  ∀ (h : ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom),
    ∃ (y : Aut F), (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) y = a
⊢ (∃ (y : Aut F), (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) y = a) ↔
    ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom

Tactic:
refine ⟨fun ⟨σ, h⟩ i ↦ by cat_disch, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom
X Y : C
f : X ⟶ Y
h₁ :
  ∀ (x : (F.obj X).obj),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
      ((@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 Y).hom) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
      ((@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))
              _ _ _ ((a X).hom ≫ F.map f) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
⊢ F.map f ≫ (a Y).hom = (a X).hom ≫ F.map f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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 Y).hom) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    ((@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))
            _ _ _ ((a X).hom ≫ F.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))

Tactic:
simpa using ConcreteCategory.congr_hom (h ⟨X, Y, f⟩) _

Premises used: CategoryTheory.Comma.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow.{u₂, u₁} C), F.map i.hom ≫ Iso.hom (a i.right) = Iso.hom (a i.left) ≫ F.map i.hom
⊢ ∃ (y : Aut F), (autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) y = a

Tactic:
exact ⟨NatIso.ofComponents a (fun {X Y} f ↦ by
    ext; simpa using ConcreteCategory.congr_hom (h ⟨X, Y, f⟩) _), rfl⟩
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
rw :
  IsClosed (X := (X : C) → Aut (F.obj X))
    (⋂ (f : Arrow.{u₂, u₁} C),
      {a : (X : C) → Aut (F.obj X) | F.map f.hom ≫ Iso.hom (a f.right) = Iso.hom (a f.left) ≫ F.map f.hom})
⊢ IsClosed (X := (X : C) → Aut (F.obj X))
    (Set.range (ι := Aut F) (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)))

Tactic:
rw [autEmbedding_range]

Premises used: CategoryTheory.PreGaloisCategory.autEmbedding_range