-- 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`. Then there exists a sub-object `Z` of `X` and an isomorphism
`Y ≅ F.obj X` as `Aut F`-sets such that the obvious triangle commutes.
-/
lemma exists_lift_of_mono (X : C) (Y : Action FintypeCat.{u} (Aut F))
    (i : Y ⟶ (functorToAction F).obj X) [Mono i] : ∃ (Z : C) (f : Z ⟶ X)
    (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Proof state:
case 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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j => Sigma.ι f j ≫ t.hom ≫ i
this : ∀ (j : ι), Mono (i' j)
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i => (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
refine ⟨∐ gZ, Sigma.desc gf, t.symm ≪≫ u' ≪≫ is2.symm, ?_, by simp [heq]⟩

Result:
case 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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j => Sigma.ι f j ≫ t.hom ≫ i
this : ∀ (j : ι), Mono (i' j)
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i => (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ Mono (Sigma.desc gf)

Proof state:
case 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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j => Sigma.ι f j ≫ t.hom ≫ i
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
have (j : ι) : Mono (i' j) :=
  have : Mono (Sigma.ι f j) := MonoCoprod.mono_ι f j
  have : Mono (t.hom ≫ i) := mono_comp _ _
  mono_comp _ _

Result:
case 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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j => Sigma.ι f j ≫ t.hom ≫ i
this : ∀ (j : ι), Mono (i' j)
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Proof state:
case 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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j => Sigma.ι f j ≫ t.hom ≫ i
this : ∀ (j : ι), Mono (i' j)
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
let u' : ∐ f ≅ ∐ fun i => (functorToAction F).obj (gZ i) := Sigma.mapIso gu

Result:
case 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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j => Sigma.ι f j ≫ t.hom ≫ i
this : ∀ (j : ι), Mono (i' j)
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i => (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Proof state:
case 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
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j => Sigma.ι f j ≫ t.hom ≫ i
this : ∀ (j : ι), Mono (i' j)
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i => (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ Mono (Sigma.desc gf)

Tactic:
exact mono_of_mono_map (functorToAction F) (heq ▸ mono_comp _ _)

Result:
no goals