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
f g : X ⟶ Y
h : F.map f = F.map g
this_1 : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
this_2 : IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))
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
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this_1 : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
this_2 : IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))
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
X : C
σ : Aut F
x : (F.obj 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))
          _ _ _ (σ.hom.app X) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X))
      x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X Y : C
σ : Aut F
f : X ⟶ Y
x : (F.obj X).obj
⊢ HSMul.hSMul (β := (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))
          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))
      (σ • x)

Tactic:
NatTrans.naturality_apply σ.hom f x

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
hc : ¬IsConnected.{u₁, u₂} X
hi : ∀ (a : IsInitial.{u₂, u₁} X), False
contrapose! :
  ∀ (hc : ∀ (Y : C) (v : Y ⟶ X) (_ : ∀ (a : IsInitial.{u₂, u₁} Y), False) (_ : Mono v), IsIso v), IsConnected.{u₁, u₂} X
⊢ ∃ (Y : C) (v : Y ⟶ X), (∀ (a : IsInitial.{u₂, u₁} Y), False) ∧ Mono v ∧ ¬IsIso v

Tactic:
contrapose! hc
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
hi : ∀ (a : IsInitial.{u₂, u₁} X), False
hc : ∀ (Y : C) (v : Y ⟶ X) (_ : ∀ (a : IsInitial.{u₂, u₁} Y), False) (_ : Mono v), IsIso v
⊢ IsConnected.{u₁, u₂} X

Tactic:
⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩

Premises used: CategoryTheory.PreGaloisCategory.IsConnected.mk
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
X : C
hi : ∀ (a : IsInitial.{u₂, u₁} X), False
hc : ∀ (Y : C) (v : Y ⟶ X) (_ : ∀ (a : IsInitial.{u₂, u₁} Y), False) (_ : Mono v), IsIso v
⊢ IsConnected.{u₁, u₂} X

Tactic:
exact ⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X Y : C
i : X ≅ Y
have : ∀ (e : (F.obj X).obj ≃ (F.obj Y).obj), Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj

Tactic:
have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
X Y : C
i : X ≅ Y
e : (F.obj X).obj ≃ (F.obj Y).obj
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj

Tactic:
Nat.card_eq_of_bijective e (Equiv.bijective e)

Premises used: Equiv.bijective, Nat.card_eq_of_bijective, 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
X Y : C
i : X ≅ Y
e : (F.obj X).obj ≃ (F.obj Y).obj
⊢ Nat.card.{w} (F.obj X).obj = Nat.card.{w} (F.obj Y).obj

Tactic:
exact Nat.card_eq_of_bijective e (Equiv.bijective e)

Premises used: Equiv.bijective, Nat.card_eq_of_bijective, 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
X : C
rw : Nonempty.{w + 2} (IsInitial (F.obj X)) ↔ IsEmpty.{w + 1} (F.obj X).obj
⊢ Nonempty (IsInitial.{u₂, u₁} X) ↔ IsEmpty.{w + 1} (F.obj X).obj

Tactic:
rw [(IsInitial.isInitialIffObj F X).nonempty_congr]

Premises used: CategoryTheory.Limits.IsInitial.isInitialIffObj, Equiv.nonempty_congr
-- 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 : C
⊢ PreservesFiniteColimits FintypeCat.incl

Tactic:
infer_instance
-- 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 : C
⊢ PreservesFiniteColimits
    (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 : PreservesFiniteColimits (forget FintypeCat) := by
    change PreservesFiniteColimits FintypeCat.incl
    infer_instance
-- 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 : 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))
⊢ ReflectsColimit (empty FintypeCat) FintypeCat.incl

Tactic:
infer_instance
-- 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 : 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))
⊢ 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
-- 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 : C
this_1 :
  PreservesFiniteColimits
    (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
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))
⊢ Nonempty.{w + 2} (IsInitial (F.obj X)) ↔ IsEmpty.{w + 1} (F.obj X).obj

Tactic:
Concrete.initial_iff_empty_of_preserves_of_reflects (F.obj X)

Premises used: CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects, CategoryTheory.Functor.obj
-- 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 : C
this_1 :
  PreservesFiniteColimits
    (forget FintypeCat (FC := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CC :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
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))
⊢ Nonempty.{w + 2} (IsInitial (F.obj X)) ↔ IsEmpty.{w + 1} (F.obj X).obj

Tactic:
exact Concrete.initial_iff_empty_of_preserves_of_reflects (F.obj X)

Premises used: CategoryTheory.Limits.Concrete.initial_iff_empty_of_preserves_of_reflects, CategoryTheory.Functor.obj
-- 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 : C
rw : (∀ (a : IsInitial.{u₂, u₁} X), False) ↔ ¬IsEmpty.{w + 1} (F.obj X).obj
⊢ (∀ (a : IsInitial.{u₂, u₁} X), False) ↔ Nonempty.{w + 1} (F.obj X).obj

Tactic:
rw [← not_isEmpty_iff]

Premises used: not_isEmpty_iff
-- 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 : C
⊢ (∀ (a : IsInitial.{u₂, u₁} X), False) ↔ ¬IsEmpty.{w + 1} (F.obj X).obj

Tactic:
⟨fun h he ↦ ?_, fun h hin ↦ h <| (initial_iff_fiber_empty F X).mp ⟨hin⟩⟩

Premises used: CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, Nonempty.intro, Iff.intro, Iff.mp
-- 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 : C
refine : ∀ (h : ∀ (a : IsInitial.{u₂, u₁} X), False) (he : IsEmpty.{w + 1} (F.obj X).obj), False
⊢ (∀ (a : IsInitial.{u₂, u₁} X), False) ↔ ¬IsEmpty.{w + 1} (F.obj X).obj

Tactic:
refine ⟨fun h he ↦ ?_, fun h hin ↦ h <| (initial_iff_fiber_empty F X).mp ⟨hin⟩⟩
-- 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 : C
h : ∀ (a : IsInitial.{u₂, u₁} X), False
he : IsEmpty.{w + 1} (F.obj X).obj
⊢ False

Tactic:
Nonempty.elim ((initial_iff_fiber_empty F X).mpr he) h

Premises used: Iff.mpr, CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, Nonempty.elim
-- 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 : C
h : ∀ (a : IsInitial.{u₂, u₁} X), False
he : IsEmpty.{w + 1} (F.obj X).obj
⊢ False

Tactic:
exact Nonempty.elim ((initial_iff_fiber_empty F X).mpr he) h

Premises used: Iff.mpr, CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, Nonempty.elim
-- 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 : C
x : (F.obj X).obj
h : IsInitial.{u₂, u₁} X
⊢ False

Tactic:
((initial_iff_fiber_empty F X).mp ⟨h⟩).false x

Premises used: IsEmpty.false
-- 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 : C
inst_3 : IsConnected.{u₁, u₂} X
by_contra : ∀ (h : ¬Nonempty.{w + 1} (F.obj X).obj), False
⊢ Nonempty.{w + 1} (F.obj X).obj

Tactic:
by_contra 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
X : C
inst_3 : IsConnected.{u₁, u₂} X
h : ¬Nonempty.{w + 1} (F.obj X).obj
have : ∀ (hin : IsInitial.{u₂, u₁} X), False
⊢ False

Tactic:
have ⟨hin⟩ : Nonempty (IsInitial X) := (initial_iff_fiber_empty F X).mpr (not_nonempty_iff.mp 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
X : C
inst_3 : IsConnected.{u₁, u₂} X
h : ¬Nonempty.{w + 1} (F.obj X).obj
hin : IsInitial.{u₂, u₁} X
⊢ False

Tactic:
IsConnected.notInitial hin

Premises used: CategoryTheory.PreGaloisCategory.IsConnected.notInitial
-- 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 : C
inst_3 : IsConnected.{u₁, u₂} X
h : ¬Nonempty.{w + 1} (F.obj X).obj
hin : IsInitial.{u₂, u₁} X
⊢ False

Tactic:
exact IsConnected.notInitial hin

Premises used: CategoryTheory.PreGaloisCategory.IsConnected.notInitial
-- 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
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
⊢ (@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

Tactic:
simp only [fiberBinaryProductEquiv, comp_obj, FintypeCat.incl_obj, Iso.toEquiv_comp,
    Equiv.symm_trans_apply, Iso.toEquiv_symm_fun]

Premises used: CategoryTheory.Functor.comp_obj, Equiv.symm_trans_apply, CategoryTheory.Iso.toEquiv_comp, CategoryTheory.Iso.toEquiv_symm_fun, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv, FintypeCat.incl_obj
-- 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.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
⊢ (@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:
change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.fst) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.prod.fst, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, 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.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
⊢ (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:
erw [PreservesLimitPair.iso_inv_fst, Types.binaryProductIso_inv_comp_fst]

Premises used: CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst, CategoryTheory.Limits.PreservesLimitPair.iso_inv_fst
-- 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.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:
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
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
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
⊢ (@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

Tactic:
simp only [fiberBinaryProductEquiv, comp_obj, FintypeCat.incl_obj, Iso.toEquiv_comp,
    Equiv.symm_trans_apply, Iso.toEquiv_symm_fun]

Premises used: CategoryTheory.Functor.comp_obj, Equiv.symm_trans_apply, CategoryTheory.Iso.toEquiv_comp, CategoryTheory.Iso.toEquiv_symm_fun, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv, FintypeCat.incl_obj