awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} I Cᵒᵖ
F : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.leftOp ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
dsimp :
  Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (g : colimit (D.leftOp ⋙ yoneda) ⟶ F) ↦ colimit.ι (D.leftOp ⋙ yoneda) (op i) ≫ g) ≫
              Iso.hom (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
        f :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.leftOp ⋙ yoneda) (op i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.leftOp ⋙ yoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
dsimp [yonedaLemma]

Premises used: CategoryTheory.yonedaLemma
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} I Cᵒᵖ
F : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.leftOp ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (g : colimit (D.leftOp ⋙ yoneda) ⟶ F) ↦ colimit.ι (D.leftOp ⋙ yoneda) (op i) ≫ g) ≫
              Iso.hom (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
        f :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
F : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D ⋙ yoneda) ⟶ F
i : I
⊢ Eq (α := ULift.{u₁, u₂} (F.obj (op (D.obj (op i)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (D.rightOp ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) :
          (a : limit (D.rightOp ⋙ F ⋙ uliftFunctor.{u₁, u₂})) → ULift.{u₁, u₂} (F.obj (op (D.obj (op i)))))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (colimitYonedaHomIsoLimitRightOp D F)) :
              TypeCat.Fun (colimit (D ⋙ yoneda) ⟶ F) (limit (D.rightOp ⋙ F ⋙ uliftFunctor.{u₁, u₂}))) :
            (a : colimit (D ⋙ yoneda) ⟶ F) → limit (D.rightOp ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
          f) :
      ULift.{u₁, u₂} (F.obj (op (D.obj (op i)))))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (D.obj (op i)))) :
              (a : (colimit (D ⋙ yoneda)).obj (op (D.obj (op i)))) → F.obj (op (D.obj (op i))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D ⋙ yoneda) (op i)) (op (D.obj (op i)))) :
                  (a : D.obj (op i) ⟶ D.obj (op i)) → (colimit (D ⋙ yoneda)).obj (op (D.obj (op i))))
                (𝟙 (D.obj (op i))) :
              (colimit (D ⋙ yoneda)).obj (op (D.obj (op i)))) } :
      ULift.{u₁, u₂} (F.obj (op (D.obj (op i)))))

Tactic:
haveI : HasColimit (D.rightOp.leftOp ⋙ yoneda) :=
    inferInstanceAs <| HasColimit (D ⋙ yoneda)
  colimitYonedaHomIsoLimit'_π_apply _ _ _ _

Premises used: CategoryTheory.Limits.colimitYonedaHomIsoLimit'_π_apply, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.rightOp, CategoryTheory.Functor.leftOp
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Full (C := Ind.{v, u} C) (Ind.inclusion C)

Tactic:
inferInstanceAs <| ((Ind.equivalence C).functor ⋙ ObjectProperty.ι _).Full

Premises used: _private.0.CategoryTheory.instFullIndFunctorOppositeTypeInclusion._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Faithful (C := Ind.{v, u} C) (Ind.inclusion C)

Tactic:
inferInstanceAs <| ((Ind.equivalence C).functor ⋙ ObjectProperty.ι _).Faithful

Premises used: _private.0.CategoryTheory.instFaithfulIndFunctorOppositeTypeInclusion._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Full (C := C) Ind.yoneda

Tactic:
inferInstanceAs <| Functor.Full <|
    ObjectProperty.lift _ CategoryTheory.yoneda isIndObject_yoneda ⋙ (Ind.equivalence C).inverse

Premises used: _private.0.CategoryTheory.instFullIndYoneda._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Faithful (C := C) Ind.yoneda

Tactic:
inferInstanceAs <| Functor.Faithful <|
    ObjectProperty.lift _ CategoryTheory.yoneda isIndObject_yoneda ⋙ (Ind.equivalence C).inverse

Premises used: _private.0.CategoryTheory.instFaithfulIndYoneda._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_3 : HasColimit F
hF : ∀ (j : J), IsIndObject (F.obj j)
⊢ IsIndObject (colimit F)

Tactic:
isIndObject_colimit _ _ hF

Premises used: CategoryTheory.Limits.isIndObject_colimit
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_3 : HasColimit F
hF : ∀ (j : J), IsIndObject (F.obj j)
⊢ IsIndObject (colimit F)

Tactic:
exact isIndObject_colimit _ _ hF

Premises used: CategoryTheory.Limits.isIndObject_colimit
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : HasLimitsOfShape.{v, v, v, u} (Discrete J) C
F : Discrete J ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : HasLimit F
hF : ∀ (j : Discrete J), IsIndObject (F.obj j)
⊢ IsIndObject (limit F)

Tactic:
isIndObject_limit_of_discrete_of_hasLimitsOfShape _ hF

Premises used: CategoryTheory.Limits.isIndObject_limit_of_discrete_of_hasLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : HasLimitsOfShape.{v, v, v, u} (Discrete J) C
F : Discrete J ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : HasLimit F
hF : ∀ (j : Discrete J), IsIndObject (F.obj j)
⊢ IsIndObject (limit F)

Tactic:
exact isIndObject_limit_of_discrete_of_hasLimitsOfShape _ hF

Premises used: CategoryTheory.Limits.isIndObject_limit_of_discrete_of_hasLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : HasLimitsOfShape.{v, v, v, u} (Discrete J) C
⊢ HasLimitsOfShape (Discrete J) (Ind.{v, u} C)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (Ind.inclusion C)

Premises used: CategoryTheory.Ind.inclusion, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfShape.{0, 0, v, u} WalkingParallelPair C
⊢ HasLimitsOfShape WalkingParallelPair (Ind.{v, u} C)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (Ind.inclusion C)

Premises used: CategoryTheory.Ind.inclusion, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteLimits.{v, u} C
⊢ HasFiniteLimits (Ind.{v, u} C)

Tactic:
hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Ind.inclusion C)

Premises used: CategoryTheory.Ind.inclusion, CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
⊢ HasLimits (Ind.{v, u} C)

Tactic:
hasLimits_of_hasLimits_createsLimits (Ind.inclusion C)

Premises used: CategoryTheory.Ind.inclusion, CategoryTheory.hasLimits_of_hasLimits_createsLimits
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
⊢ PreservesLimits (C := C) Ind.yoneda

Tactic:
letI _ : PreservesLimitsOfSize.{v, v} (Ind.yoneda ⋙ Ind.inclusion C) :=
    preservesLimits_of_natIso Ind.yonedaCompInclusion.symm
  preservesLimits_of_reflects_of_preserves Ind.yoneda (Ind.inclusion C)

Premises used: CategoryTheory.Ind.inclusion, CategoryTheory.Ind.yoneda, CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
X : Ind.{v, u} C
⊢ IsIndObject (obj (Ind.inclusion C) X)

Tactic:
X.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
⊢ RepresentablyCoflat (C := C) Ind.yoneda

Tactic:
⟨fun X => ?_⟩

Premises used: CategoryTheory.RepresentablyCoflat.mk
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
refine : ∀ (X : Ind.{v, u} C), IsFiltered (CostructuredArrow Ind.yoneda X)
⊢ RepresentablyCoflat (C := C) Ind.yoneda

Tactic:
refine ⟨fun X => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
X : Ind.{v, u} C
suffices : IsFiltered (CostructuredArrow yoneda (obj (Ind.inclusion C) X))
⊢ IsFiltered (CostructuredArrow Ind.yoneda X)

Tactic:
suffices IsFiltered (CostructuredArrow yoneda ((Ind.inclusion C).obj X)) from
    IsFiltered.of_equivalence
      ((CostructuredArrow.post Ind.yoneda (Ind.inclusion C) X).asEquivalence.trans
      (CostructuredArrow.mapNatIso Ind.yonedaCompInclusion)).symm
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
X : Ind.{v, u} C
⊢ IsFiltered (CostructuredArrow yoneda (obj (Ind.inclusion C) X))

Tactic:
((isIndObject_iff _).1 (Ind.isIndObject_inclusion_obj X)).1

Premises used: CategoryTheory.Ind.isIndObject_inclusion_obj, CategoryTheory.Limits.isIndObject_iff, And.left, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
X : Ind.{v, u} C
⊢ IsFiltered (CostructuredArrow yoneda (obj (Ind.inclusion C) X))

Tactic:
exact ((isIndObject_iff _).1 (Ind.isIndObject_inclusion_obj X)).1

Premises used: CategoryTheory.Ind.isIndObject_inclusion_obj, CategoryTheory.Limits.isIndObject_iff, And.left, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
⊢ PreservesFiniteColimits (C := C) Ind.yoneda

Tactic:
preservesFiniteColimits_of_coflat _

Premises used: CategoryTheory.preservesFiniteColimits_of_coflat
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : SmallCategory α
inst_2 : FinCategory α
inst_3 : HasLimitsOfShape.{w, w, v, u} α C
I : Type v
inst_4 : SmallCategory I
inst_5 : IsFiltered I
⊢ PreservesLimitsOfShape (C := I ⥤ C) α (Ind.lim I)

Tactic:
haveI : PreservesLimitsOfShape α (Ind.lim I ⋙ Ind.inclusion C) :=
    preservesLimitsOfShape_of_natIso Ind.limCompInclusion.symm
  preservesLimitsOfShape_of_reflects_of_preserves _ (Ind.inclusion C)

Premises used: CategoryTheory.Ind.inclusion, CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.Ind.lim
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : SmallCategory α
inst_2 : FinCategory α
inst_3 : HasColimitsOfShape.{w, w, v, u} α C
I : Type v
inst_4 : SmallCategory I
inst_5 : IsFiltered I
⊢ PreservesColimitsOfShape (C := I ⥤ C) α (Ind.lim I)

Tactic:
inferInstanceAs (PreservesColimitsOfShape α (_ ⋙ colim))

Premises used: _private.0.CategoryTheory.instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
⊢ HasColimitsOfShape (Discrete α) (Ind.{v, u} C)

Tactic:
⟨fun F => ?_⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
refine : ∀ (F : Discrete α ⥤ Ind.{v, u} C), HasColimit F
⊢ HasColimitsOfShape (Discrete α) (Ind.{v, u} C)

Tactic:
refine ⟨fun F => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Ind.{v, u} C
I : α → Type v := fun (s : α) ↦ (F.obj { as := s : Discrete α }).presentation.I
G : (s : α) → Functor.{v, v, v, u} (I s) C := fun (s : α) ↦ (F.obj { as := s }).presentation.F
refine :
  (s : Discrete α) →
    obj
        (comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
          (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim))
        s ≅
      F.obj s
⊢ comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
      (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim) ≅
    F

Tactic:
refine Discrete.natIso (fun s => ?_)

Premises used: CategoryTheory.Discrete.natIso
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Ind.{v, u} C
I : α → Type v := fun (s : α) ↦ (F.obj { as := s : Discrete α }).presentation.I
G : (s : α) → Functor.{v, v, v, u} (I s) C := fun (s : α) ↦ (F.obj { as := s }).presentation.F
s : Discrete α
refine : colimit (J := I s.as) (G s.as ⋙ Ind.yoneda) ≅ F.obj s
⊢ obj
      (comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
        (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim))
      s ≅
    F.obj s

Tactic:
refine (Functor.Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda)) ≪≫ ?_

Premises used: CategoryTheory.Pi.eval, CategoryTheory.Functor.comp, CategoryTheory.Ind.yoneda, CategoryTheory.Discrete.as, CategoryTheory.Functor.Final.colimitIso
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Ind.{v, u} C
I : α → Type v := fun (s : α) ↦ (F.obj { as := s : Discrete α }).presentation.I
G : (s : α) → Functor.{v, v, v, u} (I s) C := fun (s : α) ↦ (F.obj { as := s }).presentation.F
s : Discrete α
⊢ colimit (J := I s.as) (G s.as ⋙ Ind.yoneda) ≅ F.obj s

Tactic:
exact Ind.colimitPresentationCompYoneda _

Premises used: CategoryTheory.Ind.colimitPresentationCompYoneda
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Ind.{v, u} C
I : α → Type v := fun (s : α) ↦ (F.obj { as := s : Discrete α }).presentation.I
G : (s : α) → Functor.{v, v, v, u} (I s) C := fun (s : α) ↦ (F.obj { as := s }).presentation.F
iso : comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
    (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim) ≅
  F :=
  Discrete.natIso fun (s : Discrete α) ↦
    Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda) ≪≫
      (F.obj { as := s.as : Discrete α }).colimitPresentationCompYoneda
⊢ HasColimit F

Tactic:
hasColimit_of_iso iso.symm

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Ind.{v, u} C
I : α → Type v := fun (s : α) ↦ (F.obj { as := s : Discrete α }).presentation.I
G : (s : α) → Functor.{v, v, v, u} (I s) C := fun (s : α) ↦ (F.obj { as := s }).presentation.F
iso : comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
    (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim) ≅
  F :=
  Discrete.natIso fun (s : Discrete α) ↦
    Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda) ≪≫
      (F.obj { as := s.as : Discrete α }).colimitPresentationCompYoneda
⊢ HasColimit F

Tactic:
exact hasColimit_of_iso iso.symm

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
⊢ HasCoproducts (Ind.{v, u} C)

Tactic:
have : HasFiniteCoproducts (Ind C) :=
    ⟨fun _ => hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift)⟩
  hasCoproducts_of_finite_and_filtered

Premises used: CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered, Equiv.ulift, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Limits.HasFiniteCoproducts.mk
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} WalkingParallelPair C
⊢ HasColimitsOfShape WalkingParallelPair (Ind.{v, u} C)

Tactic:
⟨fun F => ?_⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} WalkingParallelPair C
refine : ∀ (F : WalkingParallelPair ⥤ Ind.{v, u} C), HasColimit F
⊢ HasColimitsOfShape WalkingParallelPair (Ind.{v, u} C)

Tactic:
refine ⟨fun F => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} WalkingParallelPair C
F : WalkingParallelPair ⥤ Ind.{v, u} C
obtain :
  ∀
    (P :
      IndParallelPairPresentation (A := (F.obj WalkingParallelPair.zero).obj (P := IsIndObject)) (B :=
        (F.obj WalkingParallelPair.one).obj (P := IsIndObject))
        (map (Ind.inclusion C) (F.map WalkingParallelPairHom.left) :
          Quiver.Hom (V := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (obj (Ind.inclusion C) (F.1 WalkingParallelPair.zero))
            (obj (Ind.inclusion C) (F.1 WalkingParallelPair.one)))
        (map (Ind.inclusion C) (F.map WalkingParallelPairHom.right))),
    HasColimit F
⊢ HasColimit F

Tactic:
obtain ⟨P⟩ := nonempty_indParallelPairPresentation (F.obj WalkingParallelPair.zero).2
    (F.obj WalkingParallelPair.one).2 (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.left)
    (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.right)

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Ind.inclusion, CategoryTheory.Functor.map, CategoryTheory.Limits.WalkingParallelPairHom.right, CategoryTheory.nonempty_indParallelPairPresentation, CategoryTheory.Limits.WalkingParallelPairHom.left, CategoryTheory.Functor.obj, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} WalkingParallelPair C
F : WalkingParallelPair ⥤ Ind.{v, u} C
P :
  IndParallelPairPresentation (A := (F.obj WalkingParallelPair.zero).obj (P := IsIndObject)) (B :=
    (F.obj WalkingParallelPair.one).obj (P := IsIndObject))
    (map (Ind.inclusion C) (F.map WalkingParallelPairHom.left) :
      Quiver.Hom (V := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (obj (Ind.inclusion C) (F.1 WalkingParallelPair.zero))
        (obj (Ind.inclusion C) (F.1 WalkingParallelPair.one)))
    (map (Ind.inclusion C) (F.map WalkingParallelPairHom.right))
⊢ HasColimit F

Tactic:
hasColimit_of_iso (diagramIsoParallelPair _ ≪≫ P.parallelPairIsoParallelPairCompIndYoneda)

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.IndParallelPairPresentation.parallelPairIsoParallelPairCompIndYoneda, CategoryTheory.Iso.trans
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} WalkingParallelPair C
F : WalkingParallelPair ⥤ Ind.{v, u} C
P :
  IndParallelPairPresentation (A := (F.obj WalkingParallelPair.zero).obj (P := IsIndObject)) (B :=
    (F.obj WalkingParallelPair.one).obj (P := IsIndObject))
    (map (Ind.inclusion C) (F.map WalkingParallelPairHom.left) :
      Quiver.Hom (V := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (obj (Ind.inclusion C) (F.1 WalkingParallelPair.zero))
        (obj (Ind.inclusion C) (F.1 WalkingParallelPair.one)))
    (map (Ind.inclusion C) (F.map WalkingParallelPairHom.right))
⊢ HasColimit F

Tactic:
exact hasColimit_of_iso (diagramIsoParallelPair _ ≪≫ P.parallelPairIsoParallelPairCompIndYoneda)

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.IndParallelPairPresentation.parallelPairIsoParallelPairCompIndYoneda, CategoryTheory.Iso.trans
-- Module: Mathlib.CategoryTheory.Limits.Indization.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
⊢ HasColimits (Ind.{v, u} C)

Tactic:
has_colimits_of_hasCoequalizers_and_coproducts

Premises used: CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts