awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.obj :=
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
refine_2 :
  ∀ (σ : G) (hσ : σ • x = x'),
    ∃ (a : Y.V.obj),
      (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ i.hom :
            (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
          a =
        x'
⊢ ∃ (a : Y.V.obj),
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ i.hom :
          (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
        a =
      x'

Tactic:
obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.obj :=
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
σ : G
hσ : σ • x = x'
h₁ :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ i.hom :
        (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
      (σ • y) =
    x'
⊢ ∃ (a : Y.V.obj),
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ i.hom :
          (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
        a =
      x'

Tactic:
use σ • y
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.obj :=
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
σ : G
hσ : σ • x = x'
h₁ :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ ((Y.ρ : (a : G) → End Y.V) σ ≫ i.hom : Y.V ⟶ Action.V (Action.FintypeCat.ofMulAction G X)) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
      y =
    x'
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ i.hom :
        (a : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
      (σ • y) =
    x'

Tactic:
change (Y.ρ σ ≫ i.hom) y = x'

Premises used: CategoryTheory.ConcreteCategory.hom, Action.ρ, CategoryTheory.CategoryStruct.comp, Action.Hom.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.obj :=
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
σ : G
hσ : σ • x = x'
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _
          (((Action.ρ (Action.FintypeCat.ofMulAction G X) :
                  MonoidHom.{u, u_1} G (End (Action.V (Action.FintypeCat.ofMulAction G X)))) :
                (a : G) → End (Action.FintypeCat.ofMulAction G X).V)
              σ :
            End (Action.V (Action.FintypeCat.ofMulAction G X))) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ i.hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
          y :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.V (Action.FintypeCat.ofMulAction G X))) =
    x'

Tactic:
hσ
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj
x : X.obj :=
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
        (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
        _ _ _ i.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
    y
σ : G
hσ : σ • x = x'
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _
          (((Action.ρ (Action.FintypeCat.ofMulAction G X) :
                  MonoidHom.{u, u_1} G (End (Action.V (Action.FintypeCat.ofMulAction G X)))) :
                (a : G) → End (Action.FintypeCat.ofMulAction G X).V)
              σ :
            End (Action.V (Action.FintypeCat.ofMulAction G X))) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
      ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _ i.hom :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.FintypeCat.ofMulAction G X).V)
          y :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Action.V (Action.FintypeCat.ofMulAction G X))) =
    x'

Tactic:
exact hσ
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
⊢ IsIso i.hom

Tactic:
have : IsIso i.hom := by
      refine (ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩
      · haveI : Mono i.hom := map_mono (forget₂ _ _) i
        exact ConcreteCategory.injective_of_mono_of_preservesPullback i.hom
      · letI x : X := i.hom y
        obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq G x x'
        use σ • y
        change (Y.ρ σ ≫ i.hom) y = x'
        rw [i.comm, FintypeCat.comp_apply]
        exact hσ
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : FintypeCat
inst_1 : MulAction.{u, u_1} G X.obj
inst_2 : MulAction.IsPretransitive.{u, u_1} G X.obj
h : Nonempty.{u_1 + 1} X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
this : IsIso i.hom
⊢ IsIso i

Tactic:
apply isIso_of_reflects_iso i (Action.forget _ _)

Premises used: CategoryTheory.isIso_of_reflects_iso, Action.forget
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : Nonempty.{u_1 + 1} X.V.obj
⊢ IsConnected X ↔ MulAction.IsPretransitive.{u, u_1} G X.V.obj

Tactic:
⟨fun _ ↦ pretransitive_of_isConnected G X, fun _ ↦ isConnected_of_transitive G X.V⟩

Premises used: CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected, Iff.intro, Action.V, CategoryTheory.FintypeCat.Action.isConnected_of_transitive
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
inst_4 : IsConnected Y
obtain :
  ∀
    (y :
      (obj
          (forget₂ (Action FintypeCat (Aut F)) (FC :=
            Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
            (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
            fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
          Y).obj),
    ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
      IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f

Tactic:
obtain ⟨y⟩ := nonempty_fiber_of_isConnected (forget₂ _ FintypeCat) Y

Premises used: FintypeCat, CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected, CategoryTheory.forget₂
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
inst_4 : IsConnected Y
y :
  (obj
      (forget₂ (Action FintypeCat (Aut F)) (FC :=
        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
      Y).obj
obtain :
  ∀ (Z : C) (f : Z ⟶ X) (z : (F.obj Z).obj)
    (hz :
      Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
            z :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ i.hom :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
            y :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V))
    (hc : IsConnected.{u_1, v_1} Z) (hm : Mono f),
    ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
      IsConnected.{u_1, v_1} Z ∧ Mono f ∧ i = u.hom ≫ (functorToAction F).map f
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z),
    IsConnected.{u_1, v_1} 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)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.PreGaloisCategory.fiber_in_connected_component, Action.Hom.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
inst_4 : IsConnected Y
y :
  (obj
      (forget₂ (Action FintypeCat (Aut F)) (FC :=
        Action.HomSubtype FintypeCat (Aut F) (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
          TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
        (CC := fun (X : Action FintypeCat (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
      Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (F.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Z)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        z :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ i.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
        y :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) ((functorToAction F).obj X).V)
hc : IsConnected.{u_1, v_1} Z
hm : Mono f
⊢ IsConnected ((functorToAction F).obj Z)

Tactic:
have : IsConnected ((functorToAction F).obj Z) := PreservesIsConnected.preserves
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
obtain :
  ∀ (ι : Type) (hf : Finite ι) (f : ι → Action FintypeCat (Aut F)) (t : ∐ f ≅ Y) (hc : ∀ (i : ι), IsConnected (f i)),
    ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i

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

Premises used: CategoryTheory.PreGaloisCategory.has_decomp_connected_components'
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : 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
choose :
  ∀ (gZ : (i : ι) → C) (gf : (i : ι) → gZ i ⟶ X) (gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)),
    (∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)) →
      (∀ (i : ι), Mono (gf i)) →
        ∀ (h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)),
          ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), 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)

Premises used: CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : 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
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} 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
simp : (functorToAction F).map (Sigma.desc gf) = is2.hom ≫ u'.inv ≫ t.hom ≫ i
⊢ (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_inv, CategoryTheory.Iso.trans_inv