-- Mathlib/CategoryTheory/Galois/EssSurj.lean
/-- For every open subgroup `V` of `Aut F`, there exists an `X : C` such that
`F.obj X ≅ Aut F ⧸ V` as `Aut F`-sets. -/
lemma exists_lift_of_quotient_openSubgroup (V : OpenSubgroup (Aut F)) :
    ∃ (X : C), Nonempty ((functorToAction F).obj X ≅ Aut F ⧸ₐ V.toSubgroup)

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
hn : Nonempty (F.obj (∏ᶜ fun X => ↑X)).carrier
A : C
f : A ⟶ ∏ᶜ fun X => ↑X
hgal : IsGalois A
a : (F.obj A).carrier
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
x : (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V.carrier
⊢ (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ x =
    𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V x

Tactic:
induction' x using Quotient.inductionOn with τ

Result:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
hn : Nonempty (F.obj (∏ᶜ fun X => ↑X)).carrier
A : C
f : A ⟶ ∏ᶜ fun X => ↑X
hgal : IsGalois A
a : (F.obj A).carrier
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ ⟦τ⟧ =
    𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V ⟦τ⟧

Proof state:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝¹ : ∀ (X : ↑I), IsConnected ↑X
this✝ : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
hn : Nonempty (F.obj (∏ᶜ fun X => ↑X)).carrier
A : C
f : A ⟶ ∏ᶜ fun X => ↑X
hgal : IsGalois A
a : (F.obj A).carrier
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
h1 : ∀ σ ∈ U, σ.hom.app A = 𝟙 (F.obj A)
σ : Aut F
σinU : σ ∈ U
X : C
hX : X ∈ I
x : (F.obj X).carrier
p : A ⟶ X := f ≫ Pi.π (fun Z => ↑Z) ⟨X, hX⟩
this : IsConnected X
⊢ σ.hom.app (↑⟨X, hX⟩) x = 𝟙 (F.obj ↑⟨X, hX⟩) x

Tactic:
obtain ⟨a, rfl⟩ := surjective_of_nonempty_fiber_of_isConnected F p x

Result:
case h.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝¹ : ∀ (X : ↑I), IsConnected ↑X
this✝ : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
hn : Nonempty (F.obj (∏ᶜ fun X => ↑X)).carrier
A : C
f : A ⟶ ∏ᶜ fun X => ↑X
hgal : IsGalois A
a✝ : (F.obj A).carrier
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a✝, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a✝)) :=
  fiberIsoQuotientStabilizer A a✝
hUnormal : (↑U).Normal
h1 : ∀ σ ∈ U, σ.hom.app A = 𝟙 (F.obj A)
σ : Aut F
σinU : σ ∈ U
X : C
hX : X ∈ I
p : A ⟶ X := f ≫ Pi.π (fun Z => ↑Z) ⟨X, hX⟩
this : IsConnected X
a : (F.obj A).carrier
⊢ σ.hom.app (↑⟨X, hX⟩) (F.map p a) = 𝟙 (F.obj ↑⟨X, hX⟩) (F.map p a)

Proof state:
case h.a
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
hn : Nonempty (F.obj (∏ᶜ fun X => ↑X)).carrier
A : C
f : A ⟶ ∏ᶜ fun X => ↑X
hgal : IsGalois A
a : (F.obj A).carrier
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ σ * τ ≈ τ

Tactic:
apply (QuotientGroup.leftRel_apply).mpr

Result:
case h.a
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
hn : Nonempty (F.obj (∏ᶜ fun X => ↑X)).carrier
A : C
f : A ⟶ ∏ᶜ fun X => ↑X
hgal : IsGalois A
a : (F.obj A).carrier
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ (σ * τ)⁻¹ * τ ∈ MulAction.stabilizer (Aut F) a

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝¹ : ∀ (X : ↑I), IsConnected ↑X
this✝ : ∀ (X : ↑I), Nonempty (F.obj ↑X).carrier
hn : Nonempty (F.obj (∏ᶜ fun X => ↑X)).carrier
A : C
f : A ⟶ ∏ᶜ fun X => ↑X
hgal : IsGalois A
a : (F.obj A).carrier
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
h1 : ∀ σ ∈ U, σ.hom.app A = 𝟙 (F.obj A)
h2 : ∀ σ ∈ U, ∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)
hUinV : ↑U ≤ ↑V
this : Finite (↥↑V ⧸ (↑U).subgroupOf ↑V)
⊢ ∃ X, Nonempty ((functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑V)))

Tactic:
exact ⟨colimit (quotientDiag V hUnormal u),
  ⟨preservesColimitIso (functorToAction F) (quotientDiag V hUnormal u) ≪≫
  colimit.isoColimitCocone ⟨coconeQuotientDiag hUnormal u hUinV,
  coconeQuotientDiagIsColimit hUnormal u hUinV⟩⟩⟩

Result:
no goals