-- 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
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
have heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i := by
  simp only [Iso.trans_inv, Iso.symm_inv, Category.assoc]
  rw [← Iso.inv_comp_eq]
  refine Sigma.hom_ext _ _ (fun j ↦ ?_)
  suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by
    simpa [is2, u']
  simp only [h, Iso.inv_hom_id_assoc]

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
⊢ ∃ 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)
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
choose gZ gf gu _ _ h using fun i ↦ exists_lift_of_mono_of_isConnected F X (f i) (i' i)

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)
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

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
ι : 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
j : ι
this : (functorToAction F).map (gf j) = (gu j).inv ≫ i' j
⊢ Sigma.ι (fun i => (functorToAction F).obj (gZ i)) j ≫ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (fun i => (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i

Tactic:
simpa [is2, u']

Result:
no goals

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
ι : 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
j : ι
⊢ Sigma.ι (fun i => (functorToAction F).obj (gZ i)) j ≫ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (fun i => (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i

Tactic:
suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by
  simpa [is2, u']

Result:
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
j : ι
⊢ (functorToAction F).map (gf j) = (gu j).inv ≫ i' j