-- Mathlib/CategoryTheory/Galois/Full.lean
/--
Let `X` be an object of a Galois category with fiber functor `F` and `Y` a sub-`Aut F`-set
of `F.obj X`, on which `Aut F` acts transitively (i.e. which is connected in the Galois category
of finite `Aut F`-sets). Then there exists a connected sub-object `Z` of `X` and an isomorphism
`Y ≅ F.obj X` as `Aut F`-sets such that the obvious triangle commutes.

For a version without the connectedness assumption, see `exists_lift_of_mono`.
-/
lemma exists_lift_of_mono_of_isConnected (X : C) (Y : Action FintypeCat.{u} (Aut F))
    (i : Y ⟶ (functorToAction F).obj X) [Mono i] [IsConnected Y] : ∃ (Z : C) (f : Z ⟶ X)
    (u : Y ≅ (functorToAction F).obj Z),
    IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
obtain ⟨Z, f, z, hz, hc, hm⟩ := fiber_in_connected_component F X (i.hom y)

Result:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Proof state:
case intro.intro.intro.intro.intro.intro.intro.a
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom y = z
⊢ (fun f => (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f y) i =
    (fun f => (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f y) (u.hom ≫ (functorToAction F).map f)

Tactic:
suffices h : i.hom y = F.map f z by simpa [hu]

Result:
case intro.intro.intro.intro.intro.intro.intro.a
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom y = z
⊢ i.hom y = F.map f z

Proof state:
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom y = z
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
refine ⟨Z, f, u, hc, hm, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom y = z
⊢ i = u.hom ≫ (functorToAction F).map f

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
obtain ⟨u, hu⟩ := connected_component_unique
  (forget₂ (Action FintypeCat (Aut F)) FintypeCat) (B := (functorToAction F).obj Z)
  y z i ((functorToAction F).map f) hz.symm

Result:
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom y = z
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom y = z
h : i.hom y = F.map f z
⊢ (fun f => (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f y) i =
    (fun f => (forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f y) (u.hom ≫ (functorToAction F).map f)

Tactic:
simpa [hu]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
have : IsConnected ((functorToAction F).obj Z) := PreservesIsConnected.preserves

Result:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).carrier
Z : C
f : Z ⟶ X
z : (F.obj Z).carrier
hz : F.map f z = i.hom y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
⊢ ∃ Z f u, IsConnected Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f