-- 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 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
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
⊢ (autEmbedding F) σ X = 1

Tactic:
have h : σ.hom.app X = 𝟙 (F.obj X) := by
  have : Fintype (fι ⟨X, XinI⟩) := Fintype.ofFinite _
  ext x
  obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ := Limits.FintypeCat.jointly_surjective
    (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _ (Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x
  rw [FintypeCat.id_apply, ← ha, FunctorToFintypeCat.naturality]
  simp [h ⟨(ff _) j, ⟨Set.range (ff ⟨X, XinI⟩), ⟨⟨_, rfl⟩, ⟨j, rfl⟩⟩⟩⟩]

Result:
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
h✝ : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
h : σ.hom.app X = 𝟙 (F.obj X)
⊢ (autEmbedding F) σ X = 1

Proof state:
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

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

Result:
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
⊢ ∃ 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.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
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
⊢ (autEmbedding F) σ X ∈ u X

Tactic:
suffices h : autEmbedding F σ X = 1 by
  rw [h]
  exact (ho X XinI).right

Result:
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
h : ∀ (X : ↑(⋃ X, Set.range (ff X))), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
X : C
XinI : X ∈ ↑I
⊢ (autEmbedding F) σ X = 1

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

Tactic:
obtain ⟨⟨j⟩, a, ha : F.map _ a = x⟩ := Limits.FintypeCat.jointly_surjective
  (Discrete.functor (ff ⟨X, XinI⟩) ⋙ F) _ (Limits.isColimitOfPreserves F (h4 ⟨X, XinI⟩)) x

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