awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
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 : C
this :
  PreservesFiniteColimits
    (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
⊢ Nonempty.{w + 2} (IsInitial (F.obj X)) ↔ IsEmpty.{w + 1} (F.obj X).obj
have this₁ : ReflectsColimit (empty FintypeCat)
  (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
Tactic: haveI : ReflectsColimit (Functor.empty.{0} _) (forget FintypeCat) := by
    change ReflectsColimit (Functor.empty.{0} _) FintypeCat.incl
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 : C
⊢ (∀ (a : IsInitial.{u₂, u₁} X), False) ↔ Nonempty.{w + 1} (F.obj X).obj
have rw : (∀ (a : IsInitial.{u₂, u₁} X), False) ↔ ¬IsEmpty.{w + 1} (F.obj X).obj
Tactic: rw [← not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 : C
⊢ (∀ (a : IsInitial.{u₂, u₁} X), False) ↔ ¬IsEmpty.{w + 1} (F.obj X).obj
have refine : ∀ (h : ∀ (a : IsInitial.{u₂, u₁} X), False) (he : IsEmpty.{w + 1} (F.obj X).obj), False
Tactic: refine ⟨fun h he ↦ ?_, fun h hin ↦ h <| (initial_iff_fiber_empty F X).mp ⟨hin⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 : C
inst_3 : IsConnected.{u₁, u₂} X
⊢ Nonempty.{w + 1} (F.obj X).obj
have by_contra : ∀ (h : ¬Nonempty.{w + 1} (F.obj X).obj), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 : C
inst_3 : IsConnected.{u₁, u₂} X
h : ¬Nonempty.{w + 1} (F.obj X).obj
⊢ False
have have : ∀ (hin : IsInitial.{u₂, u₁} X), False
Tactic: have ⟨hin⟩ : Nonempty (IsInitial X) := (initial_iff_fiber_empty F X).mpr (not_nonempty_iff.mp h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 _ (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.fst : F.obj (Limits.prod.{u₂, u₁} X Y) ⟶ F.obj X) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (X ⨯ Y))) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      (((Equiv.symm (fiberBinaryProductEquiv F X Y) :
              (F.obj X).obj × (F.obj Y).obj ≃ (F.obj (Limits.prod.{u₂, u₁} X Y)).obj) :
            (a : (F.obj X).obj × (F.obj Y).obj) → (F.obj (X ⨯ Y)).obj)
          (x, y) :
        (F.obj (Limits.prod.{u₂, u₁} X Y)).obj) =
    x
have simp : (@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.fst : F.obj (Limits.prod.{u₂, u₁} X Y) ⟶ F.obj X) :
      (a : (F.obj (X ⨯ Y)).obj) → (F.obj X).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))) =
  x
Tactic: simp only [fiberBinaryProductEquiv, comp_obj, FintypeCat.incl_obj, Iso.toEquiv_comp,
    Equiv.symm_trans_apply, Iso.toEquiv_symm_fun]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 _ (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.fst : F.obj (Limits.prod.{u₂, u₁} X Y) ⟶ F.obj X) :
        (a : (F.obj (X ⨯ Y)).obj) → (F.obj X).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))) =
    x
have 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.fst)) :
      (a : (fun (X : Type w) ↦ X) ((F.obj X).obj × (F.obj Y).obj)) →
        (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj X))
    (x, y) =
  x
Tactic: change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.fst) _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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)
          (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.fst)) :
        (a : (fun (X : Type w) ↦ X) ((F.obj X).obj × (F.obj Y).obj)) →
          (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj X))
      (x, y) =
    x
have erw : (ConcreteCategory.hom (FC := TypeCat.Fun) (↾_root_.Prod.fst) :
      (a : (fun (X : Type w) ↦ X) ((F.obj X).obj × (F.obj Y).obj)) →
        (fun (X : Type w) ↦ X) ((F ⋙ FintypeCat.incl).obj X))
    (x, y) =
  x
Tactic: erw [PreservesLimitPair.iso_inv_fst, Types.binaryProductIso_inv_comp_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 _ (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 : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj (X ⨯ Y))) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
      (((Equiv.symm (fiberBinaryProductEquiv F X Y) :
              (F.obj X).obj × (F.obj Y).obj ≃ (F.obj (Limits.prod.{u₂, u₁} X Y)).obj) :
            (a : (F.obj X).obj × (F.obj Y).obj) → (F.obj (X ⨯ Y)).obj)
          (x, y) :
        (F.obj (Limits.prod.{u₂, u₁} X Y)).obj) =
    y
have simp : (@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: simp only [fiberBinaryProductEquiv, comp_obj, FintypeCat.incl_obj, Iso.toEquiv_comp,
    Equiv.symm_trans_apply, Iso.toEquiv_symm_fun]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 _ (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
have 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
Tactic: change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.snd) _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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)
          (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
have 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
Tactic: erw [PreservesLimitPair.iso_inv_snd, Types.binaryProductIso_inv_comp_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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)
have apply : ∀ (a : IsInitial.{u₂, u₁} (equalizer f g)), False
Tactic: apply IsConnected.noTrivialComponent _ (equalizer.ι f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
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))
⊢ f = g
have this : 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⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 : 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
have 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)
Tactic: change Function.Injective ((fun f : A ⟶ A ↦ F.map f a) ∘ (fun f : Aut A ↦ f.hom))
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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} (α := 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)
have 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
Tactic: apply Function.Injective.comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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
⊢ 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)
have hf : Function.Injective (β := A ⟶ A) fun (f : Aut A) ↦ f.hom
Tactic: apply Function.Injective.comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (hypothesis)
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
⊢ Function.Surjective (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) (β :=
    (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj 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 X)) →
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
have this : Epi f
Tactic: have : Epi f := epi_of_nonempty_of_isConnected F f
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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
ι : Type u_1
inst_3 : Finite ι
X : ι → C
inst_4 : ∀ (i : ι), Nonempty.{w + 1} (F.obj (X i)).obj
⊢ Nonempty.{w + 1} (F.obj (piObj.{u_1, u₂, u₁} X)).obj
have intro : ∀ (val : Fintype ι), Nonempty.{w + 1} (F.obj (piObj.{u_1, u₂, u₁} X)).obj
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Galois.Basic (goal)
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 : Mono f
h : Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
⊢ IsIso (F.map f)
have apply : Function.Bijective (α := (F.obj X).obj) (β := (F.obj Y).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))
        _ _ _ (F.map f)) :
    (a : (F.obj X).obj) → (F.obj Y).obj)
Tactic: apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr