awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
⊢ Function.Injective (α :=
    obj
      (forget (Action FintypeCat G) (FC :=
        Action.HomSubtype FintypeCat G (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 G) ↦ X.V.obj))
      (Action.imageComplement G f))
    (β :=
    obj
      (forget (Action FintypeCat G) (FC :=
        Action.HomSubtype FintypeCat G (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 G) ↦ X.V.obj))
      Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (map
            (forget (Action FintypeCat G) (FC :=
              Action.HomSubtype FintypeCat G (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 G) ↦ X.V.obj))
            (Action.imageComplementIncl G f))) :
      (a : (forget (Action FintypeCat G)).obj (Action.imageComplement G f)) → (forget (Action FintypeCat G)).obj Y)

Tactic:
exact Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
obtain :
  ∀ (G' : Type) (hg : Group G') (hf : Fintype G') (e : G ≃* G'),
    HasColimitsOfShape.{u, 0, w, w + 1} (SingleObj G) FintypeCat
⊢ HasColimitsOfShape.{u, 0, w, w + 1} (SingleObj G) FintypeCat

Tactic:
obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G

Premises used: Finite.exists_type_univ_nonempty_mulEquiv
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
G' : Type
hg : Group G'
hf : Fintype G'
e : G ≃* G'
⊢ HasColimitsOfShape.{u, 0, w, w + 1} (SingleObj G) FintypeCat

Tactic:
Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

Premises used: MulEquiv.toSingleObjEquiv, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
G' : Type
hg : Group G'
hf : Fintype G'
e : G ≃* G'
⊢ HasColimitsOfShape.{u, 0, w, w + 1} (SingleObj G) FintypeCat

Tactic:
exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

Premises used: MulEquiv.toSingleObjEquiv, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
⊢ PreservesFiniteLimits (C := Action FintypeCat G) (Action.forget FintypeCat G ⋙ FintypeCat.incl)

Tactic:
apply comp_preservesFiniteLimits

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
⊢ FiberFunctor
    (forget₂ (Action FintypeCat G) (FC :=
      Action.HomSubtype FintypeCat G (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 G) ↦ 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))

Tactic:
inferInstanceAs <| FiberFunctor (Action.forget FintypeCat G)

Premises used: _private.0.CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeFunObjFiniteV._proof_1
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
have : ∀ (this : Fintype (↑T : Type u_1)), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
have : Fintype T := Fintype.ofFinite T
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
⊢ Mono i

Tactic:
have : Mono i := ConcreteCategory.mono_of_injective _ (Subtype.val_injective)
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this : Mono i
apply : ∀ (a : IsInitial T'), False
⊢ IsIso i

Tactic:
apply IsConnected.noTrivialComponent T' i

Premises used: CategoryTheory.PreGaloisCategory.IsConnected.noTrivialComponent
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this : Mono i
apply : Nonempty.{u_1 + 1} (obj (Action.forget FintypeCat G) T').obj
⊢ ∀ (a : IsInitial T'), False

Tactic:
apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr

Premises used: Iff.mpr, Action.forget, CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this : Mono i
⊢ Nonempty.{u_1 + 1} (obj (Action.forget FintypeCat G) T').obj

Tactic:
Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)

Premises used: MulAction.nonempty_orbit, Set.Nonempty.coe_sort
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this : Mono i
⊢ Nonempty.{u_1 + 1} (obj (Action.forget FintypeCat G) T').obj

Tactic:
exact Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)

Premises used: MulAction.nonempty_orbit, Set.Nonempty.coe_sort
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this : Mono i
⊢ IsIso i

Tactic:
have : IsIso i := by
      apply IsConnected.noTrivialComponent T' i
      apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr
      exact Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
apply : IsIso i.hom
⊢ Function.Bijective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) T'.V) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) 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) T'.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)

Tactic:
apply (ConcreteCategory.isIso_iff_bijective i.hom).mp

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective, Iff.mp, Action.Hom.hom
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
⊢ IsIso i.hom

Tactic:
map_isIso (forget₂ _ FintypeCat) i

Premises used: FintypeCat, CategoryTheory.forget₂, CategoryTheory.Functor.map_isIso, FintypeCat.homMk
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
⊢ IsIso i.hom

Tactic:
exact map_isIso (forget₂ _ FintypeCat) i

Premises used: FintypeCat, CategoryTheory.forget₂, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
⊢ Function.Bijective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) T'.V) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) 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) T'.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)

Tactic:
have hb : Function.Bijective i.hom := by
      apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
      exact map_isIso (forget₂ _ FintypeCat) i
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
hb :
  Function.Bijective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) T'.V) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) 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) T'.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
obtain : ∀ (y' : X.V.obj) (g : G) (hg : g • x = y') (hy' : y' = y), ∃ (g : G), g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
obtain ⟨⟨y', ⟨g, (hg : g • x = y')⟩⟩, (hy' : y' = y)⟩ := hb.surjective y

Premises used: Function.Bijective.surjective
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
hb :
  Function.Bijective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) T'.V) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) 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) T'.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
y' : X.V.obj
g : G
hg : g • x = y'
hy' : y' = y
h : g • x = y
⊢ ∃ (g : G), g • x = y

Tactic:
use g
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
hb :
  Function.Bijective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) T'.V) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) 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) T'.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
y' : X.V.obj
g : G
hg : g • x = y'
hy' : y' = y
⊢ g • x = y

Tactic:
hg.trans hy'

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X : Action FintypeCat G
inst_1 : IsConnected X
x y : X.V.obj
T : Set X.V.obj := MulAction.orbit G x
this_1 : Fintype (↑T : Type u_1)
this_2 : MulAction.{u, u_1} G (FintypeCat.of (↑T : Type u_1)).obj :=
  { toSemigroupAction := MulAction.instElemOrbit.toSemigroupAction, one_smul := ⋯ }
T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of (↑T : Type u_1))
i : T' ⟶ X := { hom := FintypeCat.homMk (Subtype.val (p := fun (x : X.V.obj) ↦ x ∈ T)), comm := ⋯ }
this_3 : Mono i
this : IsIso i
hb :
  Function.Bijective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) T'.V) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) 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) T'.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V)
y' : X.V.obj
g : G
hg : g • x = y'
hy' : y' = y
⊢ g • x = y

Tactic:
exact hg.trans hy'

Premises used: Eq.trans
-- 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
obtain : ∀ (y : Y.V.obj), IsIso i
⊢ IsIso i

Tactic:
obtain ⟨(y : Y.V)⟩ := (not_initial_iff_fiber_nonempty (Action.forget _ _) Y).mp hni

Premises used: Action.forget, CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty, Iff.mp, Action.V
-- 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:
(ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩

Premises used: Iff.mpr, CategoryTheory.ConcreteCategory.isIso_iff_bijective, And.intro, Action.Hom.hom
-- 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
refine_1 :
  Function.Injective (α := Y.V.obj) (β := (Action.V (Action.FintypeCat.ofMulAction G 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 : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)
refine_2 :
  ∀ (x' : (Action.V (Action.FintypeCat.ofMulAction G X)).obj),
    ∃ (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'
⊢ IsIso i.hom

Tactic:
refine (ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩

Premises used: Iff.mpr, CategoryTheory.ConcreteCategory.isIso_iff_bijective, And.intro, Action.Hom.hom
-- 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
⊢ Mono i.hom

Tactic:
haveI : Mono i.hom := map_mono (forget₂ _ _) i
-- 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 : Mono i.hom
⊢ Function.Injective (α := Y.V.obj) (β := (Action.V (Action.FintypeCat.ofMulAction G 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 : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)

Tactic:
ConcreteCategory.injective_of_mono_of_preservesPullback i.hom

Premises used: CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback, Action.Hom.hom
-- 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 : Mono i.hom
⊢ Function.Injective (α := Y.V.obj) (β := (Action.V (Action.FintypeCat.ofMulAction G 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 : Y.V.obj) → (Action.FintypeCat.ofMulAction G X).V.obj)

Tactic:
exact ConcreteCategory.injective_of_mono_of_preservesPullback i.hom

Premises used: CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback, Action.Hom.hom