awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
⊢ ∃ (j : CostructuredArrow yoneda (colimit F)),
    Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
        (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i) j ∧
      Nonempty.{v + 1} (A ⟶ j)

Tactic:
⟨(map (colimit.ι F i)).obj (j i y'), ?_, ⟨?_⟩⟩

Premises used: Nonempty.intro, And.intro, Exists.intro, CategoryTheory.CostructuredArrow.map, CategoryTheory.Functor.obj, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
refine_1 :
  Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
    (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i)
    (obj (CostructuredArrow.map (colimit.ι F i)) (j i y'))
refine_2 : A ⟶ obj (CostructuredArrow.map (colimit.ι F i)) (j i y')
⊢ ∃ (j : CostructuredArrow yoneda (colimit F)),
    Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
        (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i) j ∧
      Nonempty.{v + 1} (A ⟶ j)

Tactic:
refine ⟨(map (colimit.ι F i)).obj (j i y'), ?_, ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
refine_1 :
  ∃ (i_1 : I),
    ∃ x ∈ s i_1,
      Eq (α := CostructuredArrow yoneda (colimit F)) (obj (CostructuredArrow.map (colimit.ι F i_1)) x)
        (obj (CostructuredArrow.map (colimit.ι F i)) (j i y'))
⊢ Membership.mem (γ := Set (CostructuredArrow yoneda (colimit F)))
    (⋃ (i : I), obj (CostructuredArrow.map (colimit.ι F i)) '' s i)
    (obj (CostructuredArrow.map (colimit.ι F i)) (j i y'))

Tactic:
simp only [Set.mem_iUnion, Set.mem_image]

Premises used: Set.mem_iUnion, Set.mem_image
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
⊢ ∃ (i_1 : I),
    ∃ x ∈ s i_1,
      Eq (α := CostructuredArrow yoneda (colimit F)) (obj (CostructuredArrow.map (colimit.ι F i_1)) x)
        (obj (CostructuredArrow.map (colimit.ι F i)) (j i y'))

Tactic:
⟨i, j i y', hjs _ _, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
⊢ ∃ (i_1 : I),
    ∃ x ∈ s i_1,
      Eq (α := CostructuredArrow yoneda (colimit F)) (obj (CostructuredArrow.map (colimit.ι F i_1)) x)
        (obj (CostructuredArrow.map (colimit.ι F i)) (j i y'))

Tactic:
exact ⟨i, j i y', hjs _ _, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
refine_2 : A ⟶ obj (CostructuredArrow.map (colimit.ι F i)) y'
⊢ A ⟶ obj (CostructuredArrow.map (colimit.ι F i)) (j i y')

Tactic:
refine ?_ ≫ (map (colimit.ι F i)).map x

Premises used: CategoryTheory.Functor.map, CategoryTheory.CostructuredArrow.map, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
refine_2 :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left))
        (Functor.map yoneda (𝟙 A.left) ≫ CostructuredArrow.hom (obj (CostructuredArrow.map (colimit.ι F i)) y')) :
      (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
⊢ A ⟶ obj (CostructuredArrow.map (colimit.ι F i)) y'

Tactic:
refine homMk (𝟙 A.left) (yonedaEquiv.injective ?_)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CostructuredArrow.homMk, Equiv.injective, CategoryTheory.yonedaEquiv, CategoryTheory.CostructuredArrow.left
-- Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
⊢ Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left))
        (Functor.map yoneda (𝟙 A.left) ≫ CostructuredArrow.hom (obj (CostructuredArrow.map (colimit.ι F i)) y')) :
      (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))

Tactic:
simp [-EmbeddingLike.apply_eq_iff_eq, hy, yonedaEquiv_comp, y']

Premises used: EmbeddingLike.apply_eq_iff_eq, CategoryTheory.yonedaEquiv_comp
-- 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)
P : IndObjectPresentation A
⊢ IsFiltered.{v, v} P.I

Tactic:
P.hI

Premises used: CategoryTheory.Limits.IndObjectPresentation.hI
-- 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)
P : IndObjectPresentation A
⊢ P.toCostructuredArrow.Final

Tactic:
Presheaf.final_toCostructuredArrow_comp_pre _ P.coconeIsColimit

Premises used: CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre, CategoryTheory.Limits.IndObjectPresentation.coconeIsColimit, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow
-- 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)
P : IndObjectPresentation A
⊢ IsIndObject A

Tactic:
⟨⟨P⟩⟩

Premises used: CategoryTheory.Limits.IsIndObject.mk', Nonempty.intro
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsIndObject.{v, u} (Functor.obj yoneda X)

Tactic:
.mk <| IndObjectPresentation.yoneda X

Premises used: CategoryTheory.Limits.IndObjectPresentation.yoneda, CategoryTheory.Limits.IsIndObject.mk
-- Module: Mathlib.CategoryTheory.Limits.Indization.IndObject
Goal:
C : Type u
inst : Category.{v, u} C
A B : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : A ⟶ B
inst_1 : IsIso η
⊢ IsIndObject A ↔ IsIndObject B

Tactic:
⟨.map η, .map (inv η)⟩

Premises used: CategoryTheory.Limits.IsIndObject.map, Iff.intro, CategoryTheory.inv
-- 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)
h : IsIndObject A
⊢ IsFiltered (CostructuredArrow yoneda A)

Tactic:
IsFiltered.of_final h.presentation.toCostructuredArrow

Premises used: CategoryTheory.IsFiltered.of_final, CategoryTheory.Limits.IsIndObject.presentation, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow
-- 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)
h : IsIndObject A
⊢ FinallySmall (CostructuredArrow yoneda A)

Tactic:
FinallySmall.mk' h.presentation.toCostructuredArrow

Premises used: CategoryTheory.Limits.IsIndObject.presentation, CategoryTheory.FinallySmall.mk', CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow
-- 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)
⊢ 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))))

Tactic:
have h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final := Functor.final_of_natIso
    (factoringCompInclusion (fromFinalModel <| CostructuredArrow yoneda A)).symm
-- 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))))
⊢ Functor.Final (C :=
    IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
      FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
    (inclusion (fromFinalModel (CostructuredArrow yoneda A)))

Tactic:
have h₂ : Functor.Final (inclusion (fromFinalModel (CostructuredArrow yoneda A))) :=
    Functor.final_of_comp_full_faithful' (factoring _) (inclusion _)
-- 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)
⊢ Nonempty.{v + 1} (FinalModel (CostructuredArrow yoneda A))

Tactic:
have hq : Nonempty (FinalModel (CostructuredArrow yoneda A)) := Nonempty.map
    (Functor.Final.lift (fromFinalModel (CostructuredArrow yoneda A))) IsFiltered.nonempty