awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (hypothesis)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hi : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ (↑V : Set (Aut F))
this_1 : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
this : ∀ (X : (↑I : Type u₁)), Nonempty.{u₁ + 1} (F.obj (↑X : C)).obj
hn : Nonempty.{u₁ + 1} (F.obj (piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C))).obj
A : C
f : A ⟶ piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
hgal : IsGalois.{u₁, u₂} A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F)
    (FintypeCat.of (HasQuotient.Quotient (Aut F) (B := Subgroup (Aut F)) (MulAction.stabilizer (Aut F) a))) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U : Subgroup (Aut F)).Normal
h1 : ∀ (σ : Aut F) (σinU : σ ∈ U), σ.hom.app A = 𝟙 (F.obj A)
h2 : ∀ (σ : Aut F) (σinU : σ ∈ U) (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))
hUinV : (↑U : Set (Aut F)) ≤ (↑V : Set (Aut F))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))
have this₁ : Finite.{u₁ + 1}
  (HasQuotient.Quotient ↥(↑V : Subgroup (Aut F)) (B := Subgroup ↥(↑V : Subgroup (Aut F)))
    ((↑U : Subgroup (Aut F)).subgroupOf (↑V : Subgroup (Aut F))))
Tactic: have := V.quotient_finite_of_isOpen' (U.subgroupOf V) V.isOpen (V.subgroupOf_isOpen U U.isOpen)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X : Action FintypeCat (Aut F)
inst_3 : TopologicalSpace X.V.obj
inst_4 : DiscreteTopology.{u₁} X.V.obj
inst_5 : ContinuousSMul.{u₁, u₁} (Aut F) X.V.obj
⊢ ∃ (A : C), Nonempty.{u₁ + 1} ((functorToAction F).obj A ≅ X)
have obtain : ∀ (ι : Type) (hfin : Finite ι) (f : ι → OpenSubgroup (Aut F))
  (u :
    (∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑(f i) : Subgroup (Aut F))))) ≅ X),
  ∃ (A : C), Nonempty.{u₁ + 1} ((functorToAction F).obj A ≅ X)
Tactic: obtain ⟨ι, hfin, f, ⟨u⟩⟩ := has_decomp_quotients X
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.EssSurj (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X : Action FintypeCat (Aut F)
inst_3 : TopologicalSpace X.V.obj
inst_4 : DiscreteTopology.{u₁} X.V.obj
inst_5 : ContinuousSMul.{u₁, u₁} (Aut F) X.V.obj
ι : Type
hfin : Finite ι
f : ι → OpenSubgroup (Aut F)
u : (∐ fun (i : ι) ↦ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑(f i) : Subgroup (Aut F))))) ≅ X
⊢ ∃ (A : C), Nonempty.{u₁ + 1} ((functorToAction F).obj A ≅ X)
have choose : ∀ (g : (i : ι) → C)
  (gu :
    ∀ (i : ι),
      Nonempty.{u₁ + 1}
        ((functorToAction F).obj (g i) ≅
          Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑(f i) : Subgroup (Aut F)))))),
  ∃ (A : C), Nonempty.{u₁ + 1} ((functorToAction F).obj A ≅ X)
Tactic: choose g gu using (fun i ↦ exists_lift_of_quotient_openSubgroup (f i))
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
X Y : FintypeCat
f : X ⟶ Y
⊢ FintypeCat
have haveI : (this :
    Fintype
      (↑(Set.range (ι := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.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) :
                (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X) →
                  (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y))ᶜ :
        Type u)) →
  FintypeCat
Tactic: haveI : Fintype (↑(Set.range f)ᶜ) := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.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))
            _ _ _ f.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) g)) :
          (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
        (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) :
      (fun (X : Type u_1) ↦ X) Y.V.obj)
⊢ False
have apply : Membership.mem (γ := Set ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
  (Set.range (ι := (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))
          _ _ _ f.hom) :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
  (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
Tactic: apply y.property
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V
h :
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.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))
            _ _ _ f.hom :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) g)) :
          (a : (fun (X : Type u_1) ↦ X) Y.V.obj) → (fun (X : Type u_1) ↦ X) Y.V.obj)
        (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) :
      (fun (X : Type u_1) ↦ X) Y.V.obj)
⊢ Membership.mem (γ := Set ((fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
    (Set.range (ι := (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))
            _ _ _ f.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V))
    (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
have 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))
        _ _ _ f.hom :
      (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) X.V) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((X.ρ : (a : G) → End X.V) g⁻¹)) :
          (a : (fun (X : Type u_1) ↦ X) X.V.obj) → (fun (X : Type u_1) ↦ X) X.V.obj)
        x :
      (fun (X : Type u_1) ↦ X) X.V.obj) =
  (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
Tactic: use (X.ρ g⁻¹).hom x
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
⊢ Mono (Action.imageComplementIncl G f)
have apply : Mono (X :=
  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))
  (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))
Tactic: apply Functor.mono_of_mono_map (forget _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
⊢ Mono (X :=
    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))
    (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))
have i : 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: apply ConcreteCategory.mono_of_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
⊢ HasColimitsOfShape.{u, 0, w, w + 1} (SingleObj G) FintypeCat
have obtain : ∀ (G' : Type) (hg : Group G') (hf : Fintype G') (e : G ≃* G'),
  HasColimitsOfShape.{u, 0, w, w + 1} (SingleObj G) FintypeCat
Tactic: obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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
⊢ ∃ (g : G), g • x = y
have have : ∀ (this : Fintype (↑T : Type u_1)), ∃ (g : G), g • x = y
Tactic: have : Fintype T := Fintype.ofFinite T
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (hypothesis)
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 := ⋯ }
⊢ ∃ (g : G), g • x = y
have this₁ : Mono i
Tactic: have : Mono i := ConcreteCategory.mono_of_injective _ (Subtype.val_injective)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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
have apply : ∀ (a : IsInitial T'), False
Tactic: apply IsConnected.noTrivialComponent T' i
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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
⊢ ∀ (a : IsInitial T'), False
have apply : Nonempty.{u_1 + 1} (obj (Action.forget FintypeCat G) T').obj
Tactic: apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (hypothesis)
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
⊢ ∃ (g : G), g • x = y
have this₁ : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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)
have apply : IsIso i.hom
Tactic: apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (hypothesis)
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
⊢ ∃ (g : G), g • x = y
have 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)
Tactic: have hb : Function.Bijective i.hom := by
      apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
      exact map_isIso (forget₂ _ FintypeCat) i
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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)
⊢ ∃ (g : G), g • x = y
have obtain : ∀ (y' : X.V.obj) (g : G) (hg : g • x = y') (hy' : y' = y), ∃ (g : G), g • x = y
Tactic: obtain ⟨⟨y', ⟨g, (hg : g • x = y')⟩⟩, (hy' : y' = y)⟩ := hb.surjective y
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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 : G), g • x = y
have h : g • x = y
Tactic: use g
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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
⊢ IsIso i
have obtain : ∀ (y : Y.V.obj), IsIso i
Tactic: obtain ⟨(y : Y.V)⟩ := (not_initial_iff_fiber_nonempty (Action.forget _ _) Y).mp hni
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Examples (goal)
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
have 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)
Tactic: refine (ConcreteCategory.isIso_iff_bijective i.hom).mpr ⟨?_, fun x' ↦ ?_⟩