-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- The fiber of any object in a Galois category is represented by a Galois object. -/
lemma exists_galois_representative (X : C) : ∃ (A : C) (a : F.obj A),
    IsGalois A ∧ Function.Bijective (fun (f : A ⟶ X) ↦ F.map f a)

Proof state:
case h.left
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ IsGalois A

Tactic:
refine (isGalois_iff_pretransitive F A).mpr ⟨fun x y ↦ ?_⟩

Result:
case h.left
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).carrier
⊢ ∃ g, g • x = y

Proof state:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x : (F.obj X).carrier
⊢ (fun f => F.map f a) (u ≫ Pi.π (fun x => X) x) = x

Tactic:
exact (selfProdProj_fiber h1) x

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ ∃ A a, IsGalois A ∧ Function.Bijective fun f => F.map f a

Tactic:
use A

Result:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ ∃ a, IsGalois A ∧ Function.Bijective fun f => F.map f a

Proof state:
case h.right
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x : (F.obj X).carrier
⊢ ∃ a_1, (fun f => F.map f a) a_1 = x

Tactic:
use u ≫ Pi.π _ x

Result:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x : (F.obj X).carrier
⊢ (fun f => F.map f a) (u ≫ Pi.π (fun x => X) x) = x

Proof state:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ ∃ a, IsGalois A ∧ Function.Bijective fun f => F.map f a

Tactic:
use a

Result:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ IsGalois A ∧ Function.Bijective fun f => F.map f a

Proof state:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ IsGalois A ∧ Function.Bijective fun f => F.map f a

Tactic:
constructor

Result:
case h.left
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ IsGalois A

case h.right
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Bijective fun f => F.map f a

Proof state:
case h.right
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Bijective fun f => F.map f a

Tactic:
refine ⟨evaluation_injective_of_isConnected F A X a, ?_⟩

Result:
case h.right
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
⊢ Function.Surjective fun f => F.map f a

Proof state:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).carrier
fi1 : A ≅ A
hfi1 : F.map fi1.hom x = a
fi2 : A ≅ A
hfi2 : F.map fi2.hom y = a
⊢ F.map (fi1.hom ≫ fi2.inv) x = y

Tactic:
simp only [map_comp, FintypeCat.comp_apply]

Result:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).carrier
fi1 : A ≅ A
hfi1 : F.map fi1.hom x = a
fi2 : A ≅ A
hfi2 : F.map fi2.hom y = a
⊢ F.map fi2.inv (F.map fi1.hom x) = y

Proof state:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x y : (F.obj A).carrier
fi1 : A ≅ A
hfi1 : F.map fi1.hom x = a
fi2 : A ≅ A
hfi2 : F.map fi2.hom y = a
⊢ F.map fi2.inv (F.map fi2.hom y) = y

Tactic:
exact congr_fun (F.mapIso fi2).hom_inv_id y

Result:
no goals