awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
change :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.inv (Types.binaryProductIso (F.obj X).obj (F.obj Y).obj) ≫
            CategoryStruct.comp (Y := (F ⋙ FintypeCat.incl).obj (Limits.prod.{u₂, u₁} X Y))
              (Iso.inv (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y)) ((F ⋙ FintypeCat.incl).map prod.snd)) :
        (a : (fun (X : Type w) ↦ X) ((F.obj X).obj × (F.obj Y).obj)) →
          (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj Y))
      (x, y) =
    y
⊢ (@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 prod.snd : F.obj (Limits.prod.{u₂, u₁} X Y) ⟶ F.obj Y) :
        (a : (F.obj (X ⨯ Y)).obj) → (F.obj Y).obj)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y)))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (Types.binaryProductIso (F.obj X).obj (F.obj Y).obj)))
          (x, y))) =
    y

Tactic:
change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.snd) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, CategoryTheory.Limits.prod.snd, FintypeCat.incl, CategoryTheory.Limits.Types.binaryProductIso, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
erw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (↾_root_.Prod.snd) :
        (a : (fun (X : Type w) ↦ X) ((F.obj X).obj × (F.obj Y).obj)) →
          (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj Y))
      (x, y) =
    y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.inv (Types.binaryProductIso (F.obj X).obj (F.obj Y).obj) ≫
            CategoryStruct.comp (Y := (F ⋙ FintypeCat.incl).obj (Limits.prod.{u₂, u₁} X Y))
              (Iso.inv (PreservesLimitPair.iso (F ⋙ FintypeCat.incl) X Y)) ((F ⋙ FintypeCat.incl).map prod.snd)) :
        (a : (fun (X : Type w) ↦ X) ((F.obj X).obj × (F.obj Y).obj)) →
          (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj Y))
      (x, y) =
    y

Tactic:
erw [PreservesLimitPair.iso_inv_snd, Types.binaryProductIso_inv_comp_snd]

Premises used: CategoryTheory.Limits.PreservesLimitPair.iso_inv_snd, CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (↾_root_.Prod.snd) :
        (a : (fun (X : Type w) ↦ X) ((F.obj X).obj × (F.obj Y).obj)) →
          (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj Y))
      (x, y) =
    y

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
f g : A ⟶ X
h :
  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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (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 g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
apply : ∀ (a : IsInitial.{u₂, u₁} (equalizer f g)), False
⊢ IsIso (X := equalizer f g) (equalizer.ι f g)

Tactic:
apply IsConnected.noTrivialComponent _ (equalizer.ι f g)

Premises used: CategoryTheory.Limits.equalizer.ι, CategoryTheory.PreGaloisCategory.IsConnected.noTrivialComponent
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
f g : A ⟶ X
h :
  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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (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 g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ ∀ (a : IsInitial.{u₂, u₁} (equalizer f g)), False

Tactic:
not_initial_of_inhabited F ((fiberEqualizerEquiv F f g).symm ⟨a, h⟩)

Premises used: CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv, CategoryTheory.PreGaloisCategory.not_initial_of_inhabited, Subtype.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
f g : A ⟶ X
h :
  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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (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 g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ ∀ (a : IsInitial.{u₂, u₁} (equalizer f g)), False

Tactic:
exact not_initial_of_inhabited F ((fiberEqualizerEquiv F f g).symm ⟨a, h⟩)

Premises used: CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv, CategoryTheory.PreGaloisCategory.not_initial_of_inhabited, Subtype.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
f g : A ⟶ X
h :
  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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (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 g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
⊢ IsIso (X := equalizer f g) (equalizer.ι f g)

Tactic:
haveI : IsIso (equalizer.ι f g) := by
    apply IsConnected.noTrivialComponent _ (equalizer.ι f g)
    exact not_initial_of_inhabited F ((fiberEqualizerEquiv F f g).symm ⟨a, h⟩)
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
f g : A ⟶ X
h :
  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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (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 g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
this : IsIso (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
eq_of_epi_equalizer

Premises used: CategoryTheory.Limits.eq_of_epi_equalizer
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A X : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
f g : A ⟶ X
h :
  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 A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (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 g) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
        a :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
this : IsIso (X := equalizer f g) (equalizer.ι f g)
⊢ f = g

Tactic:
exact eq_of_epi_equalizer

Premises used: CategoryTheory.Limits.eq_of_epi_equalizer
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
change :
  Function.Injective.{u₂ + 1, w + 1} (α := Aut A) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    ((fun (f : A ⟶ A) ↦
        (@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 A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
          a) ∘
      fun (f : Aut A) ↦ f.hom)
⊢ Function.Injective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    fun (f : Aut A) ↦
    (@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.hom) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a

Tactic:
change Function.Injective ((fun f : A ⟶ A ↦ F.map f a) ∘ (fun f : Aut A ↦ f.hom))

Premises used: CategoryTheory.ConcreteCategory.hom, Function.comp, CategoryTheory.Functor.map, Function.Injective, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
hg :
  Function.Injective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    fun (f : A ⟶ A) ↦
    (@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 A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a
hf : Function.Injective (β := A ⟶ A) fun (f : Aut A) ↦ f.hom
⊢ Function.Injective.{u₂ + 1, w + 1} (α := Aut A) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    ((fun (f : A ⟶ A) ↦
        (@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 A)) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
          a) ∘
      fun (f : Aut A) ↦ f.hom)

Tactic:
apply Function.Injective.comp

Premises used: Function.Injective.comp
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
⊢ Function.Injective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    fun (f : A ⟶ A) ↦
    (@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 A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a

Tactic:
evaluation_injective_of_isConnected F A A a

Premises used: CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
⊢ Function.Injective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
    fun (f : A ⟶ A) ↦
    (@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 A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a

Tactic:
exact evaluation_injective_of_isConnected F A A a

Premises used: CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
⊢ Function.Injective (β := A ⟶ A) fun (f : Aut A) ↦ f.hom

Tactic:
@Aut.ext _ _ A

Premises used: CategoryTheory.Aut.ext, Function.Injective
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
A : C
inst_3 : IsConnected.{u₁, u₂} A
a : (F.obj A).obj
⊢ Function.Injective (β := A ⟶ A) fun (f : Aut A) ↦ f.hom

Tactic:
exact @Aut.ext _ _ A

Premises used: CategoryTheory.Aut.ext
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X Y : C
f : X ⟶ Y
inst_3 : Epi f
⊢ Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
    (⇑(@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 X)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))

Tactic:
surjective_of_epi (FintypeCat.incl.map (F.map f))

Premises used: CategoryTheory.Functor.map, FintypeCat.incl, CategoryTheory.surjective_of_epi
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : PreGaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
X A : C
inst_3 : Nonempty.{w + 1} (F.obj X).obj
inst_4 : IsConnected.{u₁, u₂} A
f : X ⟶ A
⊢ Epi f

Tactic:
have : Epi f := epi_of_nonempty_of_isConnected F f