awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
f : Arrow.{u₂, u₁} C
⊢ Continuous (Y := F.obj f.left ⟶ F.obj f.right) fun (a : (X : C) → Aut (F.obj X)) ↦ F.map f.hom ≫ Iso.hom (a f.right)

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
f : Arrow.{u₂, u₁} C
⊢ Continuous (Y := F.obj f.left ⟶ F.obj f.right) fun (a : (X : C) → Aut (F.obj X)) ↦ Iso.hom (a f.left) ≫ F.map f.hom

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ 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})

Tactic:
exact isClosed_iInter (fun f ↦ isClosed_eq (by fun_prop) (by fun_prop))

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

Tactic:
(autEmbedding_isClosedEmbedding F).compactSpace

Premises used: Topology.IsClosedEmbedding.compactSpace, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ T2Space (Aut F)

Tactic:
T2Space.of_injective_continuous (autEmbedding_injective F) continuous_induced_dom

Premises used: CategoryTheory.PreGaloisCategory.autEmbedding_injective, T2Space.of_injective_continuous, continuous_induced_dom
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ TotallyDisconnectedSpace (Aut F)

Tactic:
(autEmbedding_isClosedEmbedding F).isEmbedding.isTotallyDisconnected_range.mp
    (isTotallyDisconnected_of_totallyDisconnectedSpace _)

Premises used: isTotallyDisconnected_of_totallyDisconnectedSpace, Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.isTotallyDisconnected_range, Iff.mp, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ ContinuousMul (Aut F)

Tactic:
(autEmbedding_isClosedEmbedding F).isInducing.continuousMul (autEmbedding F)

Premises used: Topology.IsClosedEmbedding.isInducing, Topology.IsInducing.continuousMul, CategoryTheory.PreGaloisCategory.autEmbedding, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ ContinuousInv (Aut F)

Tactic:
(autEmbedding_isClosedEmbedding F).isInducing.continuousInv fun _ ↦ rfl

Premises used: Topology.IsClosedEmbedding.isInducing, Topology.IsInducing.continuousInv, rfl, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
⊢ IsTopologicalGroup (Aut F)

Tactic:
⟨⟩

Premises used: IsTopologicalGroup.mk
-- 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
continuous_smul : Continuous (Y := (F.obj X).obj) fun (p : Aut (F.obj X) × (F.obj X).obj) ↦ p.1 • p.2
⊢ ContinuousSMul.{w, w} (Aut (F.obj X)) (F.obj X).obj

Tactic:
constructor
-- 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
⊢ Continuous (Y := (F.obj X).obj) fun (p : Aut (F.obj X) × (F.obj X).obj) ↦ p.1 • p.2

Tactic:
fun_prop
-- 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
g : Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj :=
  fun (x : Aut (F.obj X) × (F.obj X).obj) ↦
    match (motive := Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj) x with
    | (σ, 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 :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x
h : (q : Aut F × (F.obj X).obj) → Aut (F.obj X) × (F.obj X).obj :=
  fun (q : Aut F × (F.obj X).obj) ↦
    (((fun (p : (X : C) → Aut (F.obj X)) ↦ p X) ∘ (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X))) q.1, q.2)
change : Continuous (g ∘ h)
⊢ Continuous (Y := (F.obj X).obj) fun (p : Aut F × (F.obj X).obj) ↦ p.1 • p.2

Tactic:
change Continuous (g ∘ h)

Premises used: Continuous, Function.comp
-- 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
g : Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj :=
  fun (x : Aut (F.obj X) × (F.obj X).obj) ↦
    match (motive := Aut (F.obj X) × (F.obj X).obj → (F.obj X).obj) x with
    | (σ, 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 :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        x
h : (q : Aut F × (F.obj X).obj) → Aut (F.obj X) × (F.obj X).obj :=
  fun (q : Aut F × (F.obj X).obj) ↦
    (((fun (p : (X : C) → Aut (F.obj X)) ↦ p X) ∘ (⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X))) q.1, q.2)
⊢ Continuous (g ∘ h)

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : FintypeCat ⥤ FintypeCat
rw :
  ∀ (i : C),
    Continuous (Y := Aut ((obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F).obj i)) fun (a : Aut F) ↦
      Function.comp (β := Aut (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F))
        (⇑(autEmbedding (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F)) :
          (a : Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F)) →
            (X : C) → Aut ((((whiskeringRight C FintypeCat FintypeCat).obj G).obj F).obj X))
        (⇑(mapAut F (obj (whiskeringRight C FintypeCat FintypeCat) G)) :
          (a : Aut F) → Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F))
        a i
⊢ Continuous (X := Aut F) (Y := Aut (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F))
    (⇑(mapAut F (obj (whiskeringRight C FintypeCat FintypeCat) G)) :
      (a : Aut F) → Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F))

Tactic:
rw [Topology.IsInducing.continuous_iff (autEmbedding_isClosedEmbedding _).isInducing,
    continuous_pi_iff]

Premises used: Topology.IsClosedEmbedding.isInducing, Topology.IsInducing.continuous_iff, continuous_pi_iff, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : FintypeCat ⥤ FintypeCat
X : C
change :
  Continuous (Y := Aut (G.obj (F.obj X))) fun (a : Aut F) ↦
    (mapAut (F.obj X) G : (a : Aut (F.obj X)) → Aut (G.obj (F.obj X)))
      ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) a X)
⊢ Continuous (Y := Aut ((obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F).obj X)) fun (a : Aut F) ↦
    Function.comp (β := Aut (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F))
      (⇑(autEmbedding (obj (obj (whiskeringRight C FintypeCat FintypeCat) G) F)) :
        (a : Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F)) →
          (X : C) → Aut ((((whiskeringRight C FintypeCat FintypeCat).obj G).obj F).obj X))
      (⇑(mapAut F (obj (whiskeringRight C FintypeCat FintypeCat) G)) :
        (a : Aut F) → Aut (((whiskeringRight C FintypeCat FintypeCat).obj G).obj F))
      a X

Tactic:
change Continuous fun a ↦ G.mapAut (F.obj X) (autEmbedding F a X)

Premises used: Continuous, CategoryTheory.Functor.mapAut, CategoryTheory.PreGaloisCategory.autEmbedding, DFunLike.coe, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
G : FintypeCat ⥤ FintypeCat
X : C
⊢ Continuous (Y := Aut (G.obj (F.obj X))) fun (a : Aut F) ↦
    (mapAut (F.obj X) G : (a : Aut (F.obj X)) → Aut (G.obj (F.obj X)))
      ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) a X)

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
H : Set (Aut F)
h1 : 1 ∈ H
h : IsOpen H
obtain :
  ∀ (U : Set ((X : C) → Aut (F.obj X))) (hUopen : IsOpen U)
    (h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1)
    (h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)),
    ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
      (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
        ∀ (σ : Aut F),
          (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
            Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ H

Tactic:
obtain ⟨U, hUopen, rfl⟩ := isOpen_induced_iff.mp h

Premises used: Iff.mp, isOpen_induced_iff, rfl
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
obtain :
  ∀ (I : Finset C) (u : (a : C) → Set (Aut (F.obj a))) (ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a)
    (ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U),
    ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
      (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
        ∀ (σ : Aut F),
          (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
            Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ

Tactic:
obtain ⟨I, u, ho, ha⟩ := isOpen_pi_iff.mp hUopen 1 h1

Premises used: isOpen_pi_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
choose :
  ∀ (fι : (X : ↥I) → Type) (ff : (X : ↥I) → fι X → C) (fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C))
    (h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X)))
    (h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)) (h6 : ∀ (X : ↥I), Finite (fι X)),
    ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
      (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
        ∀ (σ : Aut F),
          (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
            Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ

Tactic:
choose fι ff fc h4 h5 h6 using (fun X : I => has_decomp_connected_components X.val)

Premises used: Subtype.val, CategoryTheory.PreGaloisCategory.has_decomp_connected_components
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
refine_1 : ∀ (X : C), Membership.mem (γ := Set C) (⋃ (X : ↥I), Set.range (ff X)) X → IsConnected.{u₁, u₂} X
refine_2 :
  ∀ (σ : Aut F),
    (∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
      Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ
⊢ ∃ (I : Set C) (x : Fintype (↑I : Type u₁)),
    (∀ X ∈ I, IsConnected.{u₁, u₂} X) ∧
      ∀ (σ : Aut F),
        (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
          Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ

Tactic:
refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
X : C
Y : ↥I
hA2 : Membership.mem (γ := Set C) ((fun (X : ↥I) ↦ Set.range (ff X)) Y) X
refine_1 : ∀ (i : fι Y), IsConnected.{u₁, u₂} (ff Y i)
⊢ IsConnected.{u₁, u₂} X

Tactic:
obtain ⟨i, rfl⟩ := hA2

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
Y : ↥I
i : fι Y
⊢ IsConnected.{u₁, u₂} (ff Y i)

Tactic:
h5 Y i
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
Y : ↥I
i : fι Y
⊢ IsConnected.{u₁, u₂} (ff Y i)

Tactic:
exact h5 Y i
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
⊢ ∀ (σ : Aut F),
    (∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
      Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ

Tactic:
fun σ h ↦ ha (fun X XinI ↦ ?_)

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
refine_2 :
  ∀ (σ : Aut F) (h : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C)))
    (X : C) (XinI : X ∈ (↑I : Set C)),
    Membership.mem (α := (fun (a : C) ↦ Aut (F.obj a)) X) (u X)
      ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
⊢ ∀ (σ : Aut F),
    (∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) →
      Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) σ

Tactic:
refine fun σ h ↦ ha (fun X XinI ↦ ?_)
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h_2 : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
h :
  Eq.{w + 1} (α := Aut (F.obj X)) ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
    (1 : Aut (F.obj X))
rw : 1 ∈ u X
⊢ Membership.mem (α := (fun (a : C) ↦ Aut (F.obj a)) X) (u X)
    ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h_2 : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
h :
  Eq.{w + 1} (α := Aut (F.obj X)) ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
    (1 : Aut (F.obj X))
⊢ 1 ∈ u X

Tactic:
(ho X XinI).right

Premises used: Set.Mem, And.right
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : Membership.mem (γ := Set (Aut F)) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U) 1
h_1 : IsOpen (X := Aut F) ((⇑(autEmbedding F) : (a : Aut F) → (X : C) → Aut (F.obj X)) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I : Set C).pi (α := fun (a : C) ↦ Aut (F.obj a)) u ⊆ U
fι : (X : ↥I) → Type
ff : (X : ↥I) → fι X → C
fc : (X : ↥I) → (i : fι X) → ff X i ⟶ (↑X : C)
h4 : (X : ↥I) → Limits.IsColimit (Limits.Cofan.mk (↑X : C) (fc X))
h5 : ∀ (X : ↥I) (i : fι X), IsConnected.{u₁, u₂} (ff X i)
h6 : ∀ (X : ↥I), Finite (fι X)
σ : Aut F
h_2 : ∀ (X : (↑(⋃ (X : ↥I), Set.range (ff X)) : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
X : C
XinI : X ∈ (↑I : Set C)
h :
  Eq.{w + 1} (α := Aut (F.obj X)) ((autEmbedding F : (a : Aut F) → (X : C) → Aut (F.obj X)) σ X : Aut (F.obj X))
    (1 : Aut (F.obj X))
⊢ 1 ∈ u X

Tactic:
exact (ho X XinI).right

Premises used: And.right