awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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_2 : ∀ (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))
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))))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))

Tactic:
⟨colimit (quotientDiag V hUnormal u),
    ⟨preservesColimitIso (functorToAction F) (quotientDiag V hUnormal u) ≪≫
    colimit.isoColimitCocone ⟨coconeQuotientDiag hUnormal u hUinV,
    coconeQuotientDiagIsColimit hUnormal u hUinV⟩⟩⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, Nonempty.intro, CategoryTheory.preservesColimitIso, CategoryTheory.Limits.colimit, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Iso.trans, _private.0.CategoryTheory.PreGaloisCategory.quotientDiag, Exists.intro, _private.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiag, _private.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiagIsColimit
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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_2 : ∀ (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))
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))))
⊢ ∃ (X : C),
    Nonempty.{u₁ + 1}
      ((functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ (↑V : Subgroup (Aut F)))))

Tactic:
exact ⟨colimit (quotientDiag V hUnormal u),
    ⟨preservesColimitIso (functorToAction F) (quotientDiag V hUnormal u) ≪≫
    colimit.isoColimitCocone ⟨coconeQuotientDiag hUnormal u hUinV,
    coconeQuotientDiagIsColimit hUnormal u hUinV⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
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)
⊢ ∃ (A : C), Nonempty.{u₁ + 1} ((functorToAction F).obj A ≅ X)

Tactic:
obtain ⟨ι, hfin, f, ⟨u⟩⟩ := has_decomp_quotients X

Premises used: CategoryTheory.PreGaloisCategory.has_decomp_quotients
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
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)
⊢ ∃ (A : C), Nonempty.{u₁ + 1} ((functorToAction F).obj A ≅ X)

Tactic:
choose g gu using (fun i ↦ exists_lift_of_quotient_openSubgroup (f i))

Premises used: CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
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:
⟨∐ g, ⟨PreservesCoproduct.iso (functorToAction F) g ≪≫
    Sigma.mapIso (fun i ↦ (gu i).some) ≪≫ u⟩⟩

Premises used: Nonempty.some, CategoryTheory.Limits.PreservesCoproduct.iso, CategoryTheory.Limits.Sigma.mapIso, Nonempty.intro, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Limits.sigmaObj
-- Module: Mathlib.CategoryTheory.Galois.EssSurj
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
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:
exact ⟨∐ g, ⟨PreservesCoproduct.iso (functorToAction F) g ≪≫
    Sigma.mapIso (fun i ↦ (gu i).some) ≪≫ u⟩⟩
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
X Y : FintypeCat
f : X ⟶ Y
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
⊢ FintypeCat

Tactic:
haveI : Fintype (↑(Set.range f)ᶜ) := Fintype.ofFinite _
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
X Y : FintypeCat
f : X ⟶ Y
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:
exact FintypeCat.of (↑(Set.range f)ᶜ)

Premises used: CategoryTheory.ConcreteCategory.hom, Compl.compl, Set.Elem, Set.range, FintypeCat.of, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Examples
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)
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)
⊢ False

Tactic:
apply y.property

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Galois.Examples
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)
⊢ 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))
            _ _ _ ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V) →
            (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) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((HMul.hMul (α := End Y.V) (β := End Y.V) ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V)
                  ((Y.ρ : (a : G) → End Y.V) g : End Y.V)).hom
              (F := ObjectProperty.FullSubcategory.obj)) :
          (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)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Galois.Examples
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)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((HMul.hMul (α := End Y.V) (β := End Y.V) ((Y.ρ : (a : G) → End Y.V) g⁻¹ : End Y.V)
                ((Y.ρ : (a : G) → End Y.V) g : End Y.V)).hom
            (F := ObjectProperty.FullSubcategory.obj)) :
        (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) =
    (↑y : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) Y.V)

Tactic:
simp [← map_mul, inv_mul_cancel, Action.ρ_one, FintypeCat.id_hom]

Premises used: inv_mul_cancel, map_mul, Action.ρ_one, FintypeCat.id_hom
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
⊢ Eq.{u_1 + 1} (α := End (FintypeCat.imageComplement f.hom))
    (FintypeCat.homMk fun (y : (FintypeCat.imageComplement f.hom).obj) ↦
      Subtype.mk (p := fun (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))ᶜ
          x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (InducedCategory.Hom.hom (F := ObjectProperty.FullSubcategory.obj) ((Y.ρ : (a : G) → End Y.V) 1)) :
            (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))
        ⋯)
    1

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
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))
⊢ Mono (Action.imageComplementIncl G f)

Tactic:
apply Functor.mono_of_mono_map (forget _)

Premises used: CategoryTheory.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Galois.Examples
Goal:
G : Type u
inst : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
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)
⊢ 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 ConcreteCategory.mono_of_injective

Premises used: CategoryTheory.ConcreteCategory.mono_of_injective
-- 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:
Subtype.val_injective

Premises used: Subtype.val_injective