-- 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
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
⊢ fi1 ≪≫ fi2.symm • x = y

Tactic:
show F.map (fi1.hom ≫ fi2.inv) x = y

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 (fi1.hom ≫ fi2.inv) x = y

Proof state:
case h.left.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
x y : (F.obj A).carrier
fi1 : A ≅ A
hfi1 : F.map fi1.hom x = a
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨fi2, hfi2⟩ := subobj_selfProd_trans h1 y

Result:
case h.left.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
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
⊢ ∃ 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 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

Tactic:
rw [hfi1, ← hfi2]

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 fi2.hom y) = y

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
⊢ ∃ A a, IsGalois A ∧ Function.Bijective fun f => F.map f a

Tactic:
obtain ⟨A, u, a, h1, h2, h3⟩ := fiber_in_connected_component F (selfProd F X)
  (mkSelfProdFib F X)

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

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.Surjective fun f => F.map f a

Tactic:
intro x

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
x : (F.obj X).carrier
⊢ ∃ a_1, (fun f => F.map f a) a_1 = x

Proof state:
case h.left.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
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
⊢ ∃ g, g • x = y

Tactic:
use fi1 ≪≫ fi2.symm

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
⊢ fi1 ≪≫ fi2.symm • x = y

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
x y : (F.obj A).carrier
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨fi1, hfi1⟩ := subobj_selfProd_trans h1 x

Result:
case h.left.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
x y : (F.obj A).carrier
fi1 : A ≅ A
hfi1 : F.map fi1.hom x = a
⊢ ∃ g, g • x = y