-- 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:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
H : Set (Aut F)
h1 : 1 ∈ H
h : IsOpen H
⊢ ∃ I x, (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ H

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

Result:
case 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 x,
    (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U

Proof state:
case intro.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)
⊢ ∃ I x,
    (∀ X ∈ I, IsConnected X) ∧ ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U

Tactic:
refine ⟨⋃ X, Set.range (ff X), Fintype.ofFinite _, ?_, ?_⟩

Result:
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

case intro.intro.intro.intro.intro.refine_2
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), (∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ⇑(autEmbedding F) ⁻¹' U

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
h : (autEmbedding F) σ X = 1
⊢ (autEmbedding F) σ X ∈ u X

Tactic:
rw [h]

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
h : (autEmbedding F) σ X = 1
⊢ 1 ∈ u X

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
⊢ σ.hom.app X x = 𝟙 (F.obj X) x

Tactic:
rw [FintypeCat.id_apply, ← ha, FunctorToFintypeCat.naturality]

Result:
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