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

Tactic:
rw [← Iso.inv_comp_eq]

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
⊢ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) = u'.inv ≫ t.hom ≫ 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
⊢ (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, Category.assoc]

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
⊢ (functorToAction F).map (Sigma.desc gf) = is2.hom ≫ u'.inv ≫ t.hom ≫ 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
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
obtain ⟨ι, hf, f, t, hc⟩ := has_decomp_connected_components' Y

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