awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X_1 : C
x : F.obj X_1
X : (fromOverFunctor F x).Elements
simp_all :
  Eq (α :=
    Quiver.Hom (V := Over (F.elementsMk X_1 x))
      (Over.mk
        (homMk
          (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
            (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) :
              F.obj X.fst.left))
          (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
          ⋯))
      (Over.mk
        (homMk
          (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
            (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) :
              F.obj X.fst.left))
          (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
          ⋯)))
    (Over.homMk
      (homMk
        (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
          (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
        (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
          (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
        (𝟙 X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left) ⋯)
      ⋯)
    (𝟙
      (Over.mk
        (homMk
          (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
            (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) :
              F.obj X.fst.left))
          (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
          ⋯)))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X_1 : C
x : F.obj X_1
X : (fromOverFunctor F x).Elements
⊢ Eq (α :=
    Quiver.Hom (V := Over (F.elementsMk X_1 x))
      (Over.mk
        (homMk
          (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
            (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) :
              F.obj X.fst.left))
          (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
          ⋯))
      (Over.mk
        (homMk
          (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
            (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) :
              F.obj X.fst.left))
          (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
          ⋯)))
    (Over.homMk
      (homMk
        (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
          (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
        (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
          (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) : F.obj X.fst.left))
        (𝟙 X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left) ⋯)
      ⋯)
    (𝟙
      (Over.mk
        (homMk
          (F.elementsMk X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).left
            (↑(X.snd (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w))) :
              F.obj X.fst.left))
          (F.elementsMk X_1 x) X.fst (β := fun (c : Over.{v, u} X_1) ↦ (↑((fromOverSubfunctor F x).obj c) : Type w)).hom
          ⋯)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Functor.TypeValuedFlat
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : C
x : F.obj X
inst_1 : IsCofiltered F.Elements
⊢ IsCofiltered (fromOverFunctor F x).Elements

Tactic:
.of_equivalence (fromOverFunctorElementsEquivalence F x).symm

Premises used: CategoryTheory.FunctorToTypes.fromOverFunctorElementsEquivalence, CategoryTheory.Equivalence.symm, CategoryTheory.IsCofiltered.of_equivalence
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
⊢ functorToAction F ⋙
      forget₂ (Action FintypeCat (Aut F)) (FC :=
        Action.HomSubtype FintypeCat (Aut F) (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 (Aut F)) ↦ X.V.obj) FintypeCat (FD :=
        fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CD :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) =
    F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
X Y : C
f : X ⟶ Y
⊢ ((functorToAction F).map f).hom = F.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
inst_3 : IsGalois.{u_1, v_1} X
⊢ MulAction.IsPretransitive.{v_1, u} (Aut X) ((functorToAction F).obj X).V.obj

Tactic:
isPretransitive_of_isGalois F X

Premises used: CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
⊢ (functorToAction F).Faithful

Tactic:
have : Functor.Faithful (functorToAction F ⋙ forget₂ _ FintypeCat) :=
    inferInstanceAs <| Functor.Faithful F
  Functor.Faithful.of_comp (functorToAction F) (forget₂ _ FintypeCat)

Premises used: FintypeCat, CategoryTheory.Functor.Faithful.of_comp, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.forget₂, Action, _private.0.CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction._proof_1, CategoryTheory.Aut
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
⊢ (functorToAction F).PreservesMonomorphisms

Tactic:
have : PreservesMonomorphisms (functorToAction F ⋙ forget₂ _ FintypeCat) :=
    inferInstanceAs <| PreservesMonomorphisms F
  preservesMonomorphisms_of_preserves_of_reflects (functorToAction F) (forget₂ _ FintypeCat)

Premises used: FintypeCat, CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.forget₂, Action, _private.0.CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction._proof_1, CategoryTheory.Aut
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
⊢ (functorToAction F).ReflectsMonomorphisms

Tactic:
reflectsMonomorphisms_of_faithful _

Premises used: CategoryTheory.Functor.reflectsMonomorphisms_of_faithful
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
⊢ PreservesFiniteCoproducts (functorToAction F)

Tactic:
⟨fun _ ↦ Action.preservesColimitsOfShape_of_preserves (functorToAction F)
    (inferInstanceAs <| PreservesColimitsOfShape (Discrete _) F)⟩

Premises used: _private.0.CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction._proof_1, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.Limits.PreservesFiniteCoproducts.mk, Action.preservesColimitsOfShape_of_preserves
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
⊢ PreservesFiniteProducts (functorToAction F)

Tactic:
⟨fun _ ↦ Action.preservesLimitsOfShape_of_preserves (functorToAction F)
    (inferInstanceAs <| PreservesLimitsOfShape (Discrete _) F)⟩

Premises used: _private.0.CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction._proof_1, Action.preservesLimitsOfShape_of_preserves, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
G : Type u_2
inst_3 : Group G
inst_4 : Finite G
⊢ PreservesColimitsOfShape (SingleObj G) (functorToAction F)

Tactic:
Action.preservesColimitsOfShape_of_preserves _ <|
    inferInstanceAs <| PreservesColimitsOfShape (SingleObj G) F

Premises used: _private.0.CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite._proof_1, Action.preservesColimitsOfShape_of_preserves
-- Module: Mathlib.CategoryTheory.Galois.Action
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
⊢ PreservesIsConnected (functorToAction F)

Tactic:
⟨fun {X} _ ↦ FintypeCat.Action.isConnected_of_transitive (Aut F) (F.obj X)⟩

Premises used: CategoryTheory.PreGaloisCategory.PreservesIsConnected.mk, CategoryTheory.Aut, CategoryTheory.Functor.obj, CategoryTheory.FintypeCat.Action.isConnected_of_transitive
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : PreGaloisCategory.{u₁, u₂} C
⊢ HasFiniteLimits.{u₂, u₁} C

Tactic:
hasFiniteLimits_of_hasTerminal_and_pullbacks

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : PreGaloisCategory.{u₁, u₂} C
⊢ HasBinaryProducts.{u₂, u₁} C

Tactic:
hasBinaryProducts_of_hasTerminal_and_pullbacks C

Premises used: hasBinaryProducts_of_hasTerminal_and_pullbacks
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : PreGaloisCategory.{u₁, u₂} C
⊢ HasEqualizers.{u₂, u₁} C

Tactic:
hasEqualizers_of_hasPullbacks_and_binary_products

Premises used: CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : PreGaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : Finite G
obtain :
  ∀ (G' : Type u₂) (hg : Group G') (hf : Fintype G') (e : G ≃* G'), HasColimitsOfShape.{u_1, 0, u₂, u₁} (SingleObj G) C
⊢ HasColimitsOfShape.{u_1, 0, u₂, u₁} (SingleObj G) C

Tactic:
obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G

Premises used: Finite.exists_type_univ_nonempty_mulEquiv
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : PreGaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : Finite G
G' : Type u₂
hg : Group G'
hf : Fintype G'
e : G ≃* G'
⊢ HasColimitsOfShape.{u_1, 0, u₂, u₁} (SingleObj G) C

Tactic:
Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

Premises used: MulEquiv.toSingleObjEquiv, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Galois.Basic
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
inst_1 : PreGaloisCategory.{u₁, u₂} C
G : Type u_1
inst_2 : Group G
inst_3 : Finite G
G' : Type u₂
hg : Group G'
hf : Fintype G'
e : G ≃* G'
⊢ HasColimitsOfShape.{u_1, 0, u₂, u₁} (SingleObj G) C

Tactic:
exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

Premises used: MulEquiv.toSingleObjEquiv, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- 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
⊢ ReflectsLimitsOfShape (Discrete PEmpty.{1}) F

Tactic:
reflectsLimitsOfShape_of_reflectsIsomorphisms

Premises used: CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms
-- 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
⊢ ReflectsColimitsOfShape (Discrete PEmpty.{1}) F

Tactic:
reflectsColimitsOfShape_of_reflectsIsomorphisms

Premises used: CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms
-- 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
⊢ PreservesFiniteLimits F

Tactic:
preservesFiniteLimits_of_preservesTerminal_and_pullbacks F

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_preservesTerminal_and_pullbacks
-- 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
G : Type u_1
inst_3 : Group G
inst_4 : Finite G
choose :
  ∀ (G' : Type u₂) (hg : Group G') (hf : Fintype G') (he : Nonempty (G ≃* G')),
    PreservesColimitsOfShape.{u_1, 0, u₂, w, u₁, w + 1} (SingleObj G) F
⊢ PreservesColimitsOfShape.{u_1, 0, u₂, w, u₁, w + 1} (SingleObj G) F

Tactic:
choose G' hg hf he using Finite.exists_type_univ_nonempty_mulEquiv G

Premises used: Finite.exists_type_univ_nonempty_mulEquiv
-- 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
G : Type u_1
inst_3 : Group G
inst_4 : Finite G
G' : Type u₂
hg : Group G'
hf : Fintype G'
he : Nonempty (G ≃* G')
⊢ PreservesColimitsOfShape.{u_1, 0, u₂, w, u₁, w + 1} (SingleObj G) F

Tactic:
Limits.preservesColimitsOfShape_of_equiv he.some.toSingleObjEquiv.symm F

Premises used: MulEquiv.toSingleObjEquiv, Nonempty.some, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- 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
G : Type u_1
inst_3 : Group G
inst_4 : Finite G
G' : Type u₂
hg : Group G'
hf : Fintype G'
he : Nonempty (G ≃* G')
⊢ PreservesColimitsOfShape.{u_1, 0, u₂, w, u₁, w + 1} (SingleObj G) F

Tactic:
exact Limits.preservesColimitsOfShape_of_equiv he.some.toSingleObjEquiv.symm F

Premises used: MulEquiv.toSingleObjEquiv, Nonempty.some, CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm
-- 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
_ : Mono (F.map f) → Mono f
⊢ Mono (F.map f) → Mono f

Tactic:
_
-- 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
h : Mono (F.map f)
⊢ IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))

Tactic:
haveI : IsIso (pullback.fst (F.map f) (F.map f)) :=
    isIso_fst_of_mono (F.map f)
-- 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
h : Mono (F.map f)
this : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
rw :
  IsIso (X := F.obj (pullback f f))
    (CategoryStruct.comp (Y := pullback (F.map f) (F.map f)) (Iso.hom (PreservesPullback.iso F f f))
      (pullback.fst (F.map f) (F.map f)))
⊢ IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))

Tactic:
rw [← PreservesPullback.iso_hom_fst]

Premises used: CategoryTheory.Limits.PreservesPullback.iso_hom_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
f : X ⟶ Y
h : Mono (F.map f)
this : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
⊢ IsIso (X := F.obj (pullback f f))
    (CategoryStruct.comp (Y := pullback (F.map f) (F.map f)) (Iso.hom (PreservesPullback.iso F f f))
      (pullback.fst (F.map f) (F.map f)))

Tactic:
IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- 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
h : Mono (F.map f)
this : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
⊢ IsIso (X := F.obj (pullback f f))
    (CategoryStruct.comp (Y := pullback (F.map f) (F.map f)) (Iso.hom (PreservesPullback.iso F f f))
      (pullback.fst (F.map f) (F.map f)))

Tactic:
exact IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- 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
h : Mono (F.map f)
this : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
⊢ IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))

Tactic:
haveI : IsIso (F.map (pullback.fst f f)) := by
    rw [← PreservesPullback.iso_hom_fst]
    exact IsIso.comp_isIso
-- 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
h : Mono (F.map f)
this_1 : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
this : IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))
⊢ IsIso (X := pullback f f) (pullback.fst f f)

Tactic:
haveI : IsIso (pullback.fst f f) := isIso_of_reflects_iso (pullback.fst _ _) F
-- 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
h : Mono (F.map f)
this_1 : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
this_2 : IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))
this : IsIso (X := pullback f f) (pullback.fst f f)
⊢ Mono f

Tactic:
(pullback.diagonal_isKernelPair f).mono_of_isIso_fst

Premises used: CategoryTheory.Limits.pullback.diagonal_isKernelPair, CategoryTheory.IsKernelPair.mono_of_isIso_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
f : X ⟶ Y
h : Mono (F.map f)
this_1 : IsIso (X := pullback (F.map f) (F.map f)) (pullback.fst (F.map f) (F.map f))
this_2 : IsIso (X := F.obj (pullback f f)) (F.map (pullback.fst f f))
this : IsIso (X := pullback f f) (pullback.fst f f)
⊢ Mono f

Tactic:
exact (pullback.diagonal_isKernelPair f).mono_of_isIso_fst

Premises used: CategoryTheory.Limits.pullback.diagonal_isKernelPair, CategoryTheory.IsKernelPair.mono_of_isIso_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
f g : X ⟶ Y
h : F.map f = F.map g
⊢ IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))

Tactic:
haveI : IsIso (equalizer.ι (F.map f) (F.map g)) := equalizer.ι_of_eq 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 Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
rw :
  IsIso (X := F.obj (equalizer f g))
    (CategoryStruct.comp (Y := equalizer (F.map f) (F.map g)) (equalizerComparison f g F)
      (equalizer.ι (F.map f) (F.map g)))
⊢ IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))

Tactic:
rw [← equalizerComparison_comp_π f g F]

Premises used: CategoryTheory.Limits.equalizerComparison_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
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
this : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
⊢ IsIso (X := F.obj (equalizer f g))
    (CategoryStruct.comp (Y := equalizer (F.map f) (F.map g)) (equalizerComparison f g F)
      (equalizer.ι (F.map f) (F.map g)))

Tactic:
IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- 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 : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
⊢ IsIso (X := F.obj (equalizer f g))
    (CategoryStruct.comp (Y := equalizer (F.map f) (F.map g)) (equalizerComparison f g F)
      (equalizer.ι (F.map f) (F.map g)))

Tactic:
exact IsIso.comp_isIso

Premises used: CategoryTheory.IsIso.comp_isIso
-- 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 : IsIso (X := equalizer (F.map f) (F.map g)) (equalizer.ι (F.map f) (F.map g))
⊢ IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))

Tactic:
haveI : IsIso (F.map (equalizer.ι f g)) := by
      rw [← equalizerComparison_comp_π f g F]
      exact IsIso.comp_isIso
-- 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 : IsIso (X := F.obj (equalizer f g)) (F.map (equalizer.ι f g))
⊢ IsIso (X := equalizer f g) (equalizer.ι f g)

Tactic:
haveI : IsIso (equalizer.ι f g) := isIso_of_reflects_iso _ F