-- Mathlib/CategoryTheory/Galois/Topology.lean
/--
If `H` is an open subset of `Aut F` such that `1 ∈ H`, there exists a finite
set `I` of connected objects of `C` such that every `σ : Aut F` that induces the identity
on `F.obj X` for all `X ∈ I` is contained in `H`. In other words: The kernel
of the evaluation map `Aut F →* ∏ X : I ↦ Aut (F.obj X)` is contained in `H`.
-/
lemma exists_set_ker_evaluation_subset_of_isOpen
    {H : Set (Aut F)} (h1 : 1 ∈ H) (h : IsOpen H) :
    ∃ (I : Set C) (_ : Fintype I), (∀ X ∈ I, IsConnected X) ∧
      (∀ σ : Aut F, (∀ X : I, σ.hom.app X = 𝟙 (F.obj X)) → σ ∈ H)

Proof state:
case h.intro.mk.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha✝ : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
this : Fintype (fι ⟨X, XinI⟩)
x : (F.obj X).carrier
j : fι ⟨X, XinI⟩
a : ((Discrete.functor (ff ⟨X, XinI⟩) ⋙ F).obj { as := j }).carrier
ha : F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }) a = x
⊢ F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j })
      (σ.hom.app ((Discrete.functor (ff ⟨X, XinI⟩)).obj { as := j }) a) =
    F.map ((Limits.Cofan.mk (↑⟨X, XinI⟩) (fc ⟨X, XinI⟩)).ι.app { as := j }) a

Tactic:
simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.refine_1.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
Y : { x // x ∈ I }
i : fι Y
⊢ IsConnected (ff Y i)

Tactic:
exact h5 Y i

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.refine_1.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
X : C
Y : { x // x ∈ I }
hA2 : X ∈ (fun X => Set.range (ff X)) Y
⊢ IsConnected X

Tactic:
obtain ⟨i, rfl⟩ := hA2

Result:
case intro.intro.intro.intro.intro.refine_1.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
Y : { x // x ∈ I }
i : fι Y
⊢ IsConnected (ff Y i)

Proof state:
case intro.intro.intro.intro.intro.refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
⊢ ∀ X ∈ ⋃ X, Set.range (ff X), IsConnected X

Tactic:
rintro X ⟨A, ⟨Y, rfl⟩, hA2⟩

Result:
case intro.intro.intro.intro.intro.refine_1.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
X : C
Y : { x // x ∈ I }
hA2 : X ∈ (fun X => Set.range (ff X)) Y
⊢ IsConnected X

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
⊢ σ.hom.app X = 𝟙 (F.obj X)

Tactic:
have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
U : Set ((X : C) → Aut (F.obj X))
hUopen : IsOpen U
h1 : 1 ∈ ⇑(autEmbedding F) ⁻¹' U
h✝ : IsOpen (⇑(autEmbedding F) ⁻¹' U)
I : Finset C
u : (a : C) → Set (Aut (F.obj a))
ho : ∀ a ∈ I, IsOpen (u a) ∧ 1 a ∈ u a
ha : (↑I).pi u ⊆ U
fι : { x // x ∈ I } → Type
ff : (X : { x // x ∈ I }) → fι X → C
fc : (X : { x // x ∈ I }) → (i : fι X) → ff X i ⟶ ↑X
h4 : (X : { x // x ∈ I }) → Limits.IsColimit (Limits.Cofan.mk (↑X) (fc X))
h5 : ∀ (X : { x // x ∈ I }) (i : fι X), IsConnected (ff X i)
h6 : ∀ (X : { x // x ∈ I }), Finite (fι X)
σ : Aut F
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
this : Fintype (fι ⟨X, XinI⟩)
⊢ σ.hom.app X = 𝟙 (F.obj X)