awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
f : obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u) ≅ ⊤_ Type u
⊢ PreservesLimit.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (empty (C ⥤ Type u)) colim

Tactic:
apply preservesTerminal_of_iso

Premises used: CategoryTheory.Limits.preservesTerminal_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
f : ⊤_ Type u ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
⊢ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u) ≅ ⊤_ Type u

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
f : PUnit.{u + 1} ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
apply : ⊤_ Type u ≅ PUnit.{u + 1}
⊢ ⊤_ Type u ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)

Tactic:
apply (_ : ⊤_ (Type u) ≅ PUnit.{u + 1}).trans
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
t :
  (k : C) →
    IsLimit (F := comp (D := C ⥤ Type u) (empty (C ⥤ Type u)) (obj (evaluation C (Type u)) k))
      (mapCone (obj (evaluation C (Type u)) k) (asEmptyCone (Types.constPUnitFunctor C)))
⊢ PUnit.{u + 1} ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)

Tactic:
apply_rules [(Types.colimitConstPUnitIsoPUnit C).symm.trans, HasColimit.isoOfNatIso,
      IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits, CategoryTheory.Limits.IsTerminal.uniqueUpToIso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Limits.terminalIsTerminal, CategoryTheory.Limits.HasColimit.isoOfNatIso, CategoryTheory.Limits.Types.colimitConstPUnitIsoPUnit
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ (k : C) →
    IsLimit (F := comp (D := C ⥤ Type u) (empty (C ⥤ Type u)) (obj (evaluation C (Type u)) k))
      (mapCone (obj (evaluation C (Type u)) k) (asEmptyCone (Types.constPUnitFunctor C)))

Tactic:
exact fun _ ↦ isLimitChangeEmptyCone _ Types.isTerminalPUnit _ <| Iso.refl _

Premises used: CategoryTheory.Limits.isLimitChangeEmptyCone, CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.pt, CategoryTheory.Limits.Types.isTerminalPUnit, PUnit, CategoryTheory.Limits.asEmptyCone
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ ⊤_ Type u ≅ PUnit.{u + 1}

Tactic:
exact Types.isTerminalEquivIsoPUnit (⊤_ (Type u)) |>.toFun terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim

Tactic:
preservesLimitsOfShape_pempty_of_preservesTerminal _

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := C ⥤ Type u) colim

Tactic:
PreservesFiniteProducts.of_preserves_binary_and_terminal colim

Premises used: CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal, CategoryTheory.Limits.colim
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete WalkingPair) colim
I : (d : C × C) → colimit (Functor.diag C ⋙ obj coyoneda (op d)) ≅ PUnit.{u + 1}
⊢ IsSiftedOrEmpty C

Tactic:
apply final_of_colimit_comp_coyoneda_iso_pUnit

Premises used: CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete WalkingPair) colim
c₁ c₂ : C
⊢ colimit (Functor.diag C ⋙ obj coyoneda (op (c₁, c₂))) ≅ PUnit.{u + 1}

Tactic:
calc colimit <| diag C ⋙ coyoneda.obj (op (c₁, c₂))
    _ ≅ colimit <| _ ⋙ (coyoneda.obj _) ⊠ (coyoneda.obj _) :=
      HasColimit.isoOfNatIso <| isoWhiskerLeft _ <| .refl _
    _ ≅ colimit (_ ⊗ _) := HasColimit.isoOfNatIso <| .refl _
    _ ≅ (colimit _) ⊗ (colimit _) := CartesianMonoidalCategory.prodComparisonIso colim _ _
    _ ≅ PUnit ⊗ PUnit :=
      (Coyoneda.colimitCoyonedaIso _) ⊗ᵢ (Coyoneda.colimitCoyonedaIso _)
    _ ≅ PUnit := λ_ _

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.colim, CategoryTheory.MonoidalCategoryStruct.leftUnitor, Prod.mk, CategoryTheory.Limits.colimit, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.CartesianMonoidalCategory.prodComparisonIso, PUnit, Opposite.op, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.Coyoneda.colimitCoyonedaIso, CategoryTheory.Limits.HasColimit.isoOfNatIso, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
h : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := C ⥤ Type u) colim
⊢ IsSiftedOrEmpty C

Tactic:
isSiftedOrEmpty_of_colim_preservesBinaryProducts C

Premises used: CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesBinaryProducts
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
connected : IsConnected C
⊢ Nonempty C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
suffices : IsConnected C
⊢ Nonempty C

Tactic:
suffices connected : IsConnected C by infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
rw : Nonempty.{u + 1} (colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1})
⊢ IsConnected C

Tactic:
rw [Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit]

Premises used: CategoryTheory.Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
val : colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1}
⊢ Nonempty.{u + 1} (colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1})

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
⊢ PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim

Tactic:
haveI : PreservesLimitsOfShape (Discrete PEmpty) (colim : (C ⥤ _) ⥤ Type u) :=
    preservesLimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv') _
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
val : colimit (J := C) (⊤_ C ⥤ Type u) ≅ PUnit.{u + 1}
apply : Iso (C := C ⥤ Type u) (Types.constPUnitFunctor C) (⊤_ C ⥤ Type u)
⊢ colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1}

Tactic:
apply HasColimit.isoOfNatIso (_ : Types.constPUnitFunctor C ≅ (⊤_ (C ⥤ Type u))) |>.trans
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
val : ⊤_ Type u ≅ PUnit.{u + 1}
⊢ colimit (J := C) (⊤_ C ⥤ Type u) ≅ PUnit.{u + 1}

Tactic:
apply PreservesTerminal.iso colim |>.trans

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Limits.PreservesTerminal.iso, CategoryTheory.Iso.trans
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
⊢ ⊤_ Type u ≅ PUnit.{u + 1}

Tactic:
exact Types.terminalIso

Premises used: CategoryTheory.Limits.Types.terminalIso
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
t :
  (k : C) →
    IsLimit (F := comp (D := C ⥤ Type u) (empty (C ⥤ Type u)) (obj (evaluation C (Type u)) k))
      (mapCone (obj (evaluation C (Type u)) k) (asEmptyCone (Types.constPUnitFunctor C)))
⊢ Iso (C := C ⥤ Type u) (Types.constPUnitFunctor C) (⊤_ C ⥤ Type u)

Tactic:
apply_rules [IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]

Premises used: CategoryTheory.Limits.evaluationJointlyReflectsLimits, CategoryTheory.Limits.IsTerminal.uniqueUpToIso, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
k : C
⊢ IsLimit (F := comp (D := C ⥤ Type u) (empty (C ⥤ Type u)) (obj (evaluation C (Type u)) k))
    (mapCone (obj (evaluation C (Type u)) k) (asEmptyCone (Types.constPUnitFunctor C)))

Tactic:
exact isLimitChangeEmptyCone _ Types.isTerminalPUnit _ <| Iso.refl _

Premises used: CategoryTheory.Limits.isLimitChangeEmptyCone, CategoryTheory.Iso.refl, CategoryTheory.Limits.Types.isTerminalPUnit
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
h : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := C ⥤ Type u) colim
⊢ IsSiftedOrEmpty C

Tactic:
have := isSiftedOrEmpty_of_colim_preservesFiniteProducts C
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
h : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := C ⥤ Type u) colim
this : IsSiftedOrEmpty C
⊢ Nonempty C

Tactic:
have := nonempty_of_colim_preservesLimitsOfShapeFinZero C
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
h : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := C ⥤ Type u) colim
this_1 : IsSiftedOrEmpty C
this : Nonempty C
⊢ IsSifted C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
inst_2 : IsSifted C
F : C ⥤ D
inst_3 : F.Final
⊢ PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := D ⥤ Type u) colim

Tactic:
have : PreservesFiniteProducts (colim : (D ⥤ Type u) ⥤ _) :=
    ⟨fun n ↦ preservesLimitsOfShape_of_natIso (Final.colimIso F)⟩
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
inst_2 : IsSifted C
F : C ⥤ D
inst_3 : F.Final
this : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := D ⥤ Type u) colim
⊢ IsSifted D

Tactic:
of_colim_preservesFiniteProducts D

Premises used: CategoryTheory.IsSifted.of_colim_preservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
inst_2 : IsSifted C
F : C ⥤ D
inst_3 : F.Final
this : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := D ⥤ Type u) colim
⊢ IsSifted D

Tactic:
exact of_colim_preservesFiniteProducts D

Premises used: CategoryTheory.IsSifted.of_colim_preservesFiniteProducts
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
h₁ : IsSifted.{v, u} C
F : Functor.{v, v₁, u, u₁} C D
inst_2 : F.Final
rw : ∀ (h₁ : IsSifted (AsSmall C)) (F : Functor.{v, v₁, u, u₁} C D) [F.Final], IsSifted (AsSmall D)
⊢ IsSifted.{v₁, u₁} D

Tactic:
rw [isSifted_iff_asSmallIsSifted] at h₁ ⊢

Premises used: CategoryTheory.IsSifted.isSifted_iff_asSmallIsSifted
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
h₁ : IsSifted (AsSmall C)
F : Functor.{v, v₁, u, u₁} C D
inst_2 : F.Final
⊢ IsSifted (AsSmall D)

Tactic:
of_final_functor_from_sifted' <|
    AsSmall.equiv.{_, _, max u₁ v₁}.inverse ⋙ F ⋙ AsSmall.equiv.{_, _, max u v}.functor

Premises used: CategoryTheory.IsSifted.of_final_functor_from_sifted', CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.AsSmall.equiv, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Sifted
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
h₁ : IsSifted (AsSmall C)
F : Functor.{v, v₁, u, u₁} C D
inst_2 : F.Final
⊢ IsSifted (AsSmall D)

Tactic:
exact of_final_functor_from_sifted' <|
    AsSmall.equiv.{_, _, max u₁ v₁}.inverse ⋙ F ⋙ AsSmall.equiv.{_, _, max u v}.functor

Premises used: CategoryTheory.IsSifted.of_final_functor_from_sifted'
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : HasLimitsOfShape.{v₁, u₁, v₂, u₂} J C
⊢ HasLimitsOfShape.{v₁, u₁, v₂, u₂} J (Skeleton.{v₂, u₂} C)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (fromSkeleton C)

Premises used: CategoryTheory.fromSkeleton, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : HasLimitsOfSize.{w, w', v₂, u₂} C
⊢ HasLimitsOfSize.{w, w', v₂, u₂} (Skeleton.{v₂, u₂} C)

Tactic:
hasLimits_of_hasLimits_createsLimits (fromSkeleton C)

Premises used: CategoryTheory.hasLimits_of_hasLimits_createsLimits, CategoryTheory.fromSkeleton
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : HasLimits.{v₂, u₂} C
⊢ HasLimits.{v₂, u₂} (Skeleton.{v₂, u₂} C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} J C
⊢ HasColimitsOfShape.{v₁, u₁, v₂, u₂} J (Skeleton.{v₂, u₂} C)

Tactic:
hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (fromSkeleton C)

Premises used: CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape, CategoryTheory.fromSkeleton
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : HasColimitsOfSize.{w, w', v₂, u₂} C
⊢ HasColimitsOfSize.{w, w', v₂, u₂} (Skeleton.{v₂, u₂} C)

Tactic:
hasColimits_of_hasColimits_createsColimits (fromSkeleton C)

Premises used: CategoryTheory.hasColimits_of_hasColimits_createsColimits, CategoryTheory.fromSkeleton
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : HasColimits.{v₂, u₂} C
⊢ HasColimits.{v₂, u₂} (Skeleton.{v₂, u₂} C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : Quiver.IsThin.{u₂, v₂} C
inst_4 : HasLimitsOfShape.{v₁, u₁, v₂, u₂} J C
⊢ HasLimitsOfShape.{v₁, u₁, u₂, u₂} J (ThinSkeleton.{v₂, u₂} C)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (fromThinSkeleton C)

Premises used: CategoryTheory.ThinSkeleton.fromThinSkeleton, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : Quiver.IsThin.{u₂, v₂} C
inst_4 : HasLimitsOfSize.{w, w', v₂, u₂} C
⊢ HasLimitsOfSize.{w, w', u₂, u₂} (ThinSkeleton.{v₂, u₂} C)

Tactic:
hasLimits_of_hasLimits_createsLimits (fromThinSkeleton C)

Premises used: CategoryTheory.ThinSkeleton.fromThinSkeleton, CategoryTheory.hasLimits_of_hasLimits_createsLimits
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : Quiver.IsThin.{u₂, v₂} C
inst_4 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} J C
⊢ HasColimitsOfShape.{v₁, u₁, u₂, u₂} J (ThinSkeleton.{v₂, u₂} C)

Tactic:
hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (fromThinSkeleton C)

Premises used: CategoryTheory.ThinSkeleton.fromThinSkeleton, CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Skeleton
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
inst_3 : Quiver.IsThin.{u₂, v₂} C
inst_4 : HasColimitsOfSize.{w, w', v₂, u₂} C
⊢ HasColimitsOfSize.{w, w', u₂, u₂} (ThinSkeleton.{v₂, u₂} C)

Tactic:
hasColimits_of_hasColimits_createsColimits (fromThinSkeleton C)

Premises used: CategoryTheory.ThinSkeleton.fromThinSkeleton, CategoryTheory.hasColimits_of_hasColimits_createsColimits
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
by_contra : ∀ (r_ne_s : ¬r = s), False
⊢ r = s

Tactic:
by_contra r_ne_s
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
rw : ∃ (x : X ⟶ Y) (y : X ⟶ Y), x ≠ y
⊢ 2 ≤ #(X ⟶ Y)

Tactic:
rw [Cardinal.two_le_iff]

Premises used: Cardinal.two_le_iff
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ (x : X ⟶ Y) (y : X ⟶ Y), x ≠ y

Tactic:
⟨_, _, r_ne_s⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ (x : X ⟶ Y) (y : X ⟶ Y), x ≠ y

Tactic:
exact ⟨_, _, r_ne_s⟩
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ 2 ≤ #(X ⟶ Y)

Tactic:
have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
apply : HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
⊢ False

Tactic:
apply not_le_of_gt (Cardinal.cantor α)

Premises used: Cardinal.cantor, not_le_of_gt
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
apply : Cardinal.{u}
apply₁ : HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
apply₂ : #(X ⟶ yp) ≤ α
⊢ HPow.hPow (α := Cardinal.{u}) 2 α ≤ α

Tactic:
apply _root_.trans _ _

Premises used: trans
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ Cardinal.{u}

Tactic:
exact #(X ⟶ yp)

Premises used: Quiver.Hom
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
apply : #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)
⊢ HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)

Tactic:
apply le_trans (Cardinal.power_le_power_right z)

Premises used: Cardinal.power_le_power_right, le_trans
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
rw : #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)
⊢ #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)

Tactic:
rw [Cardinal.power_def]

Premises used: Cardinal.power_def
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
hab : #(md → (X ⟶ Y)) = #(X ⟶ yp)
⊢ #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
hab : Nonempty.{u + 1} ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
⊢ #(md → (X ⟶ Y)) = #(X ⟶ yp)

Tactic:
rw [Cardinal.eq]

Premises used: Cardinal.eq
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ Nonempty.{u + 1} ((md → (X ⟶ Y)) ≃ (X ⟶ yp))

Tactic:
⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩

Premises used: Equiv.mk, CategoryTheory.Limits.Pi.π, Nonempty.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.Pi.lift
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
hab : Function.LeftInverse (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) Pi.lift
hab₁ : Function.RightInverse (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) Pi.lift
⊢ Nonempty.{u + 1} ((md → (X ⟶ Y)) ≃ (X ⟶ yp))

Tactic:
refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : md → (X ⟶ Y)
hab : ∀ (k : md), (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) (Pi.lift f) k = f k
⊢ (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) (Pi.lift f) = f

Tactic:
ext k
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : md → (X ⟶ Y)
k : md
⊢ (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) (Pi.lift f) k = f k

Tactic:
simp [yp]