awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_1 : IsFiltered (CostructuredArrow yoneda A)
inst_2 : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  Functor.Final (C := FinalModel (CostructuredArrow yoneda A))
    (Functor.comp (D :=
      IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
        FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
      (factoring (fromFinalModel (CostructuredArrow yoneda A)))
      (inclusion (fromFinalModel (CostructuredArrow yoneda A))))
h₂ :
  Functor.Final (C :=
    IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
      FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
    (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
c : Cocone (J :=
  IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D := FinalModel (CostructuredArrow yoneda A))
    (fromFinalModel (CostructuredArrow yoneda A)))
  (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Equiv.symm
        (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
          (Presheaf.tautologicalCocone A)) :
      (a : IsColimit (Presheaf.tautologicalCocone A)) →
        IsColimit
          (Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)))
    (Presheaf.isColimitTautologicalCocone A)
hq : Nonempty.{v + 1} (FinalModel (CostructuredArrow yoneda A))
⊢ IsIndObject A

Tactic:
⟨_, inclusion (fromFinalModel _) ⋙ CostructuredArrow.proj yoneda A, c.ι, hc⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Limits.IsIndObject.mk', Nonempty.intro, CategoryTheory.fromFinalModel, CategoryTheory.Limits.Cocone.ι, CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion, CategoryTheory.Limits.IndObjectPresentation.mk, CategoryTheory.CostructuredArrow.proj
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_1 : IsFiltered (CostructuredArrow yoneda A)
inst_2 : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  Functor.Final (C := FinalModel (CostructuredArrow yoneda A))
    (Functor.comp (D :=
      IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
        FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
      (factoring (fromFinalModel (CostructuredArrow yoneda A)))
      (inclusion (fromFinalModel (CostructuredArrow yoneda A))))
h₂ :
  Functor.Final (C :=
    IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
      FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
    (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
c : Cocone (J :=
  IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D := FinalModel (CostructuredArrow yoneda A))
    (fromFinalModel (CostructuredArrow yoneda A)))
  (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Equiv.symm
        (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
          (Presheaf.tautologicalCocone A)) :
      (a : IsColimit (Presheaf.tautologicalCocone A)) →
        IsColimit
          (Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)))
    (Presheaf.isColimitTautologicalCocone A)
hq : Nonempty.{v + 1} (FinalModel (CostructuredArrow yoneda A))
⊢ IsIndObject A

Tactic:
exact ⟨_, inclusion (fromFinalModel _) ⋙ CostructuredArrow.proj yoneda A, c.ι, hc⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
⊢ IsIndObject A ↔ IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A)

Tactic:
⟨fun h => ⟨h.isFiltered, h.finallySmall⟩,
   fun ⟨_, _⟩ => isIndObject_of_isFiltered_of_finallySmall A⟩

Premises used: CategoryTheory.Limits.IsIndObject.isFiltered, CategoryTheory.Limits.IsIndObject, CategoryTheory.Limits.IsIndObject.finallySmall, CategoryTheory.Limits.isIndObject_of_isFiltered_of_finallySmall, _private.0.CategoryTheory.Limits.isIndObject_iff.match_1, And.intro, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
F : Functor.{v', v, u', u} J C
inst_2 : HasLimit F
⊢ IsIndObject (limit (F ⋙ yoneda))

Tactic:
IsIndObject.map (preservesLimitIso yoneda F).hom (isIndObject_yoneda (limit F))

Premises used: CategoryTheory.Limits.IsIndObject.map, CategoryTheory.yoneda, CategoryTheory.Limits.limit, CategoryTheory.Limits.isIndObject_yoneda, CategoryTheory.preservesLimitIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) ↔
    PreservesFiniteLimits A

Tactic:
⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩

Premises used: CategoryTheory.Limits.PreservesFiniteLimits, And.intro, Iff.intro, _private.0.CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimits.match_1
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
refine_1 :
  IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) →
    ∀ (h₁ : IsFiltered.{u, u} (CostructuredArrow yoneda A)) (h₂ : FinallySmall.{u, u, u} (CostructuredArrow yoneda A)),
      PreservesFiniteLimits A
refine_2 : ∀ (h : PreservesFiniteLimits A), IsFiltered.{u, u} (CostructuredArrow yoneda A)
refine_3 : ∀ (h : PreservesFiniteLimits A), FinallySmall.{u, u, u} (CostructuredArrow yoneda A)
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) ↔
    PreservesFiniteLimits A

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A)
h₁ : IsFiltered.{u, u} (CostructuredArrow yoneda A)
h₂ : FinallySmall.{u, u, u} (CostructuredArrow yoneda A)
⊢ PreservesFiniteLimits A

Tactic:
apply preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda

Premises used: CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A)

Tactic:
isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A

Premises used: CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A)

Tactic:
exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A

Premises used: CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ EssentiallySmall.{u, u, u} (CostructuredArrow yoneda A)

Tactic:
have := essentiallySmallSelf (CostructuredArrow yoneda A)
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
this : EssentiallySmall.{u, u, u} (CostructuredArrow yoneda A)
⊢ FinallySmall.{u, u, u} (CostructuredArrow yoneda A)

Tactic:
apply finallySmall_of_essentiallySmall

Premises used: CategoryTheory.finallySmall_of_essentiallySmall
-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : HasColimitsOfShape.{v₁, u₁, v, v + 1} I (Type v)
inst_3 : HasLimitsOfShape.{v₁, u₁, v, v + 1} Iᵒᵖ (Type v)
inst_4 : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : Functor.{v₁, v, u₁, u} I C
G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
⊢ ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    Eq.{v + 1} (α := (F.op ⋙ G).obj i)
      (ULift.down.{u, v}
        (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryStruct.comp (Y := uliftFunctor.{u, v}.obj (limit (F.op ⋙ G)))
                  (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)))
                  (uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i))) :
              TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))
      (ULift.down.{u, v}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))

Tactic:
have (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) := congrArg ULift.down
    (ConcreteCategory.congr_hom (preservesLimitIso_inv_π uliftFunctor.{u, v} (F.op ⋙ G) i) a)
-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : HasColimitsOfShape.{v₁, u₁, v, v + 1} I (Type v)
inst_3 : HasLimitsOfShape.{v₁, u₁, v, v + 1} Iᵒᵖ (Type v)
inst_4 : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : Functor.{v₁, v, u₁, u} I C
G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    Eq.{v + 1} (α := (F.op ⋙ G).obj i)
      (ULift.down.{u, v}
        (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryStruct.comp (Y := uliftFunctor.{u, v}.obj (limit (F.op ⋙ G)))
                  (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)))
                  (uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i))) :
              TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))
      (ULift.down.{u, v}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))
⊢ Eq (α := G.obj (op (F.obj (unop i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F.op ⋙ G) i) :
          (a : limit (F.op ⋙ G)) → G.obj (op (F.obj (unop i))))
        (ULift.down.{u, v}
          (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G))) :
                TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (ULift.{u, v} (limit (F.op ⋙ G)))) :
              (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → ULift.{u, v} (limit (F.op ⋙ G)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm)) :
                (a : limit (F.op ⋙ G ⋙ uliftFunctor.{u, v})) → limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}))
              (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (colimitYonedaHomIsoLimitOp F G)) :
                    TypeCat.Fun (colimit (F ⋙ yoneda) ⟶ G) (limit (F.op ⋙ G ⋙ uliftFunctor.{u, v}))) :
                  (a : colimit (F ⋙ yoneda) ⟶ G) → limit (F.op ⋙ G ⋙ uliftFunctor.{u, v}))
                η)))) :
      G.obj (op (F.obj (unop i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (F.obj (unop i)))) :
          (a : (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) → G.obj (op (F.obj (unop i))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (colimit.ι (F ⋙ yoneda) (unop i)) (op (F.obj (unop i)))) :
              (a : F.obj (unop i) ⟶ F.obj (unop i)) → (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i))))
            (𝟙 (F.obj (unop i))) :
          (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) :
      G.obj (op (F.obj (unop i))))

Tactic:
Eq.trans (dsimp% this _) ?_

Premises used: id, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : HasColimitsOfShape.{v₁, u₁, v, v + 1} I (Type v)
inst_3 : HasLimitsOfShape.{v₁, u₁, v, v + 1} Iᵒᵖ (Type v)
inst_4 : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : Functor.{v₁, v, u₁, u} I C
G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    Eq.{v + 1} (α := (F.op ⋙ G).obj i)
      (ULift.down.{u, v}
        (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryStruct.comp (Y := uliftFunctor.{u, v}.obj (limit (F.op ⋙ G)))
                  (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)))
                  (uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i))) :
              TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))
      (ULift.down.{u, v}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))
⊢ Eq (α := G.obj (op (F.obj (unop i))))
    (ULift.down.{u, v}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ULift.{u, v} (G.obj (op (F.obj (unop i)))))) :
            (a : ULift.{u, v} (G.obj (op (F.obj (unop i))))) → ULift.{u, v} (G.obj (op (F.obj (unop i)))))
          {
            down :=
              (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (F.obj (unop i)))) :
                  (a : (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) → G.obj (op (F.obj (unop i))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (NatTrans.app (colimit.ι (F ⋙ yoneda) (unop i)) (op (F.obj (unop i)))) :
                      (a : F.obj (unop i) ⟶ F.obj (unop i)) → (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i))))
                    (𝟙 (F.obj (unop i))) :
                  (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) }) :
      G.obj (op (F.obj (unop i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (F.obj (unop i)))) :
          (a : (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) → G.obj (op (F.obj (unop i))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (colimit.ι (F ⋙ yoneda) (unop i)) (op (F.obj (unop i)))) :
              (a : F.obj (unop i) ⟶ F.obj (unop i)) → (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i))))
            (𝟙 (F.obj (unop i))) :
          (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) :
      G.obj (op (F.obj (unop i))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
Goal:
C : Type u
inst : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) IsIndObject
obtain : ∀ (P : IndObjectPresentation (X.obj (P := IsIndObject))), Small.{v, max u v} (X ⟶ Y)
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
obtain ⟨⟨P⟩⟩ := X.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
Goal:
C : Type u
inst : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) IsIndObject
P : IndObjectPresentation (X.obj (P := IsIndObject))
obtain : ∀ (Q : IndObjectPresentation (Y.obj (P := IsIndObject))), Small.{v, max u v} (X ⟶ Y)
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
obtain ⟨⟨Q⟩⟩ := Y.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
Goal:
C : Type u
inst : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) IsIndObject
P : IndObjectPresentation (X.obj (P := IsIndObject))
Q : IndObjectPresentation (Y.obj (P := IsIndObject))
e₁ : { pt := X.obj (P := IsIndObject), ι := P.ι : Cocone (P.F ⋙ yoneda) }.pt ≅ (colimit.cocone (P.F ⋙ yoneda)).pt :=
  P.isColimit.coconePointUniqueUpToIso (colimit.isColimit (P.F ⋙ yoneda))
e₂ : { pt := Y.obj (P := IsIndObject), ι := Q.ι : Cocone (Q.F ⋙ yoneda) }.pt ≅ (colimit.cocone (Q.F ⋙ yoneda)).pt :=
  Q.isColimit.coconePointUniqueUpToIso (colimit.isColimit (Q.F ⋙ yoneda))
e₃ : (X.obj (P := IsIndObject) ⟶ Y.obj (P := IsIndObject)) ≃ (colimit (P.F ⋙ yoneda) ⟶ colimit (Q.F ⋙ yoneda)) :=
  e₁.homCongr e₂
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
small_map (InducedCategory.homEquiv.trans e₃)

Premises used: CategoryTheory.InducedCategory.homEquiv, Equiv.trans, small_map
-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
Goal:
C : Type u
inst : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) IsIndObject
P : IndObjectPresentation (X.obj (P := IsIndObject))
Q : IndObjectPresentation (Y.obj (P := IsIndObject))
e₁ : { pt := X.obj (P := IsIndObject), ι := P.ι : Cocone (P.F ⋙ yoneda) }.pt ≅ (colimit.cocone (P.F ⋙ yoneda)).pt :=
  P.isColimit.coconePointUniqueUpToIso (colimit.isColimit (P.F ⋙ yoneda))
e₂ : { pt := Y.obj (P := IsIndObject), ι := Q.ι : Cocone (Q.F ⋙ yoneda) }.pt ≅ (colimit.cocone (Q.F ⋙ yoneda)).pt :=
  Q.isColimit.coconePointUniqueUpToIso (colimit.isColimit (Q.F ⋙ yoneda))
e₃ : (X.obj (P := IsIndObject) ⟶ Y.obj (P := IsIndObject)) ≃ (colimit (P.F ⋙ yoneda) ⟶ colimit (Q.F ⋙ yoneda)) :=
  e₁.homCongr e₂
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
exact small_map (InducedCategory.homEquiv.trans e₃)

Premises used: CategoryTheory.InducedCategory.homEquiv, Equiv.trans, small_map
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P : IndParallelPairPresentation f g
⊢ IsFiltered.{v₁, v₁} P.I

Tactic:
P.hI

Premises used: CategoryTheory.IndParallelPairPresentation.hI
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
⊢ ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
        h.left ≫
      x_1.hom =
    x.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right

Tactic:
have := h.w
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
this :
  ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
        h.left ≫
      x_1.hom =
    x.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right
⊢ P₁.F.map h.left ≫ x_1.hom.1.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
    P₁.F.map h.left ≫ x_1.hom.2.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left

Tactic:
simp only [prod'_obj, comp_obj, prod'_map, Functor.comp_map, prod_comp, Prod.hom_ext_iff,
      CostructuredArrow.hom_eq_iff, CostructuredArrow.map_obj_left,
      IndObjectPresentation.toCostructuredArrow_obj_left, CostructuredArrow.comp_left,
      CostructuredArrow.map_map_left, IndObjectPresentation.toCostructuredArrow_map_left] at this

Premises used: CategoryTheory.CostructuredArrow.hom_eq_iff, CategoryTheory.Functor.comp_obj, CategoryTheory.CostructuredArrow.map_obj_left, CategoryTheory.Functor.prod'_obj, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_left, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_map_left, CategoryTheory.Prod.hom_ext_iff, CategoryTheory.CostructuredArrow.comp_left, CategoryTheory.Functor.prod'_map, CategoryTheory.CostructuredArrow.map_map_left, CategoryTheory.prod_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
this :
  P₁.F.map h.left ≫ x_1.hom.1.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
    P₁.F.map h.left ≫ x_1.hom.2.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.1.left = x.hom.1.left ≫ (F₂ f g P₁ P₂).map h

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
this :
  P₁.F.map h.left ≫ x_1.hom.1.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
    P₁.F.map h.left ≫ x_1.hom.2.left =
      (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.1.left = x.hom.1.left ≫ (F₂ f g P₁ P₂).map h

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ f = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)

Tactic:
(isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁
-- Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
refine :
  ∀ (i : K f g P₁ P₂),
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ f =
      { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
        (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)
⊢ f = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)

Tactic:
refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁