awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
x : Functor.{v, v', u, u'} Cᵒᵖ A
h :
  ∀ (X : C) (x_1 : Φ.fiber.obj X),
    Eq (α :=
      x.obj (Opposite.op X) ⟶
        tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber x) (tensorUnit.{v', u'} A (𝒞 := inst_1)))
      (Φ.toPresheafFiber X x_1 x ≫ Iso.inv (ρ_ (obj Φ.presheafFiber x)))
      (CategoryStruct.comp (Y := obj Φ.presheafFiber x) (Φ.toPresheafFiber X x_1 x)
        (map Φ.presheafFiber (Iso.inv (ρ_ x)) ≫
          Φ.presheafFiberDesc
              (fun (X : C) (x_2 : Φ.fiber.obj X) ↦
                Φ.toPresheafFiber X x_2 x ⊗ₘ
                  Φ.toPresheafFiber X x_2 ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)))
              ⋯ ≫
            obj Φ.presheafFiber x ◁
              Φ.presheafFiberDesc
                (fun (x : C) (x_2 : Φ.fiber.obj x) ↦
                  𝟙 (obj.{v, v', u, u'} ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)) (Opposite.op x)))
                ⋯))
⊢ Eq (α :=
    obj Φ.presheafFiber x ⟶
      tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber x) (tensorUnit.{v', u'} A (𝒞 := inst_1)))
    (Iso.inv (ρ_ (obj Φ.presheafFiber x)))
    (map Φ.presheafFiber (Iso.inv (ρ_ x)) ≫
      Φ.presheafFiberDesc
          (fun (X : C) (x_1 : Φ.fiber.obj X) ↦
            Φ.toPresheafFiber X x_1 x ⊗ₘ Φ.toPresheafFiber X x_1 ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)))
          ⋯ ≫
        obj Φ.presheafFiber x ◁
          Φ.presheafFiberDesc
            (fun (x : C) (x_1 : Φ.fiber.obj x) ↦
              𝟙 (obj.{v, v', u, u'} ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)) (Opposite.op x)))
            ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
x : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
x_1 : Φ.fiber.obj X
⊢ Eq (α :=
    x.obj (Opposite.op X) ⟶
      tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber x) (tensorUnit.{v', u'} A (𝒞 := inst_1)))
    (Φ.toPresheafFiber X x_1 x ≫ Iso.inv (ρ_ (obj Φ.presheafFiber x)))
    (CategoryStruct.comp (Y := obj Φ.presheafFiber x) (Φ.toPresheafFiber X x_1 x)
      (map Φ.presheafFiber (Iso.inv (ρ_ x)) ≫
        Φ.presheafFiberDesc
            (fun (X : C) (x_2 : Φ.fiber.obj X) ↦
              Φ.toPresheafFiber X x_2 x ⊗ₘ
                Φ.toPresheafFiber X x_2 ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)))
            ⋯ ≫
          obj Φ.presheafFiber x ◁
            Φ.presheafFiberDesc
              (fun (x : C) (x_2 : Φ.fiber.obj x) ↦
                𝟙 (obj.{v, v', u, u'} ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)) (Opposite.op x)))
              ⋯))

Tactic:
simp [tensorHom_def, ← MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
X : C
x : Φ.fiber.obj X
⊢ Eq.{v' + 1} (α :=
    obj.{v, v', u, u'} ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)) (Opposite.op X) ⟶
      tensorUnit.{v', u'} A (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
        obj (C := Functor.{v, v', u, u'} Cᵒᵖ A) Φ.presheafFiber ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)))
        (Φ.toPresheafFiber X x ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)))
        (OplaxMonoidal.η Φ.presheafFiber) :
      obj.{v, v', u, u'} ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)) (Opposite.op X) ⟶
        tensorUnit.{v', u'} A (𝒞 := inst_1))
    (𝟙 (tensorUnit.{v', u'} A (𝒞 := inst_1)) :
      tensorUnit.{v', u'} A (𝒞 := inst_1) ⟶ tensorUnit.{v', u'} A (𝒞 := inst_1))

Tactic:
toPresheafFiber_presheafFiberDesc _ _ _ _ _

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
X : C
x : Φ.fiber.obj X
G₁ G₂ : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ Eq (α :=
    (tensorObj (𝒞 := category) G₁ G₂).obj (Opposite.op X) ⟶
      tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber G₁) (obj Φ.presheafFiber G₂))
    (CategoryStruct.comp (Y := obj Φ.presheafFiber (tensorObj (𝒞 := category) G₁ G₂))
      (Φ.toPresheafFiber X x (tensorObj (𝒞 := category) G₁ G₂)) (OplaxMonoidal.δ Φ.presheafFiber G₁ G₂))
    (Φ.toPresheafFiber X x G₁ ⊗ₘ Φ.toPresheafFiber X x G₂)

Tactic:
toPresheafFiber_presheafFiberDesc _ _ _ _ _

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : LocallySmall.{w, v, u} C
inst_5 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_6 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
M : A
⊢ PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ (obj (Functor.flip (curriedTensor A)) M)

Tactic:
Final.preservesColimitsOfShape_of_final (FinallySmall.fromFilteredFinalModel.{w} _) _

Premises used: CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final, CategoryTheory.FinallySmall.fromFilteredFinalModel
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : LocallySmall.{w, v, u} C
inst_5 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_6 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
M : A
⊢ PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ (obj (curriedTensor A) M)

Tactic:
Final.preservesColimitsOfShape_of_final (FinallySmall.fromFilteredFinalModel.{w} _) _

Premises used: CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final, CategoryTheory.FinallySmall.fromFilteredFinalModel
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : LocallySmall.{w, v, u} C
inst_5 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_6 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
⊢ IsIso.{v', u'} (C := A) (X :=
    obj (C := Functor.{v, v', u, u'} Cᵒᵖ A) Φ.presheafFiber ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category))) (Y :=
    tensorUnit.{v', u'} A (𝒞 := inst_1)) (OplaxMonoidal.η Φ.presheafFiber)

Tactic:
(IsColimit.coconePointUniqueUpToIso (Φ.isColimitPresheafFiberCocone (𝟙_ _))
    (isColimitConstCocone _ (𝟙_ A))).isIso_hom

Premises used: CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit, CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.constCocone, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.isColimitConstCocone, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc, CategoryTheory.NatTrans.id, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : LocallySmall.{w, v, u} C
inst_5 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_6 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
P₁ P₂ : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ IsIso (X := obj Φ.presheafFiber (tensorObj (𝒞 := category) P₁ P₂)) (Y :=
    tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber P₁) (obj Φ.presheafFiber P₂))
    (OplaxMonoidal.δ Φ.presheafFiber P₁ P₂)

Tactic:
(IsColimit.coconePointUniqueUpToIso (Φ.isColimitPresheafFiberCocone (P₁ ⊗ P₂))
    ((Φ.isColimitPresheafFiberCocone P₁).tensor (Φ.isColimitPresheafFiberCocone P₂))).isIso_hom

Premises used: CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberCocone, CategoryTheory.Limits.IsColimit.tensor, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit, CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.colimit.desc, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc, CategoryTheory.Limits.Cocone.tensor, CategoryTheory.Monoidal.FunctorCategory.tensorObj, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : LocallySmall.{w, v, u} C
inst_5 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_6 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
X : C
x : Φ.fiber.obj X
⊢ Eq.{v' + 1} (α :=
    tensorUnit.{v', u'} A (𝒞 := inst_1) ⟶
      obj (C := Functor.{v, v', u, u'} Cᵒᵖ A) Φ.presheafFiber ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)))
    (LaxMonoidal.ε Φ.presheafFiber) (Φ.toPresheafFiber X x ((𝟙_ (Functor.{v, v', u, u'} Cᵒᵖ A)) (𝒞 := category)))

Tactic:
simp [← cancel_mono (OplaxMonoidal.η Φ.presheafFiber)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.GrothendieckTopology.Point.presheafFiber, CategoryTheory.Functor.OplaxMonoidal.η
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : LocallySmall.{w, v, u} C
inst_5 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_6 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
X : C
x : Φ.fiber.obj X
G₁ G₂ : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ Eq (α :=
    tensorObj.{v', u'} (𝒞 := inst_1) (G₁.obj (Opposite.op X)) (G₂.obj (Opposite.op X)) ⟶
      obj Φ.presheafFiber (tensorObj (𝒞 := category) G₁ G₂))
    ((Φ.toPresheafFiber X x G₁ ⊗ₘ Φ.toPresheafFiber X x G₂) ≫ LaxMonoidal.μ Φ.presheafFiber G₁ G₂)
    (Φ.toPresheafFiber X x (tensorObj (𝒞 := category) G₁ G₂))

Tactic:
simp [← cancel_mono (OplaxMonoidal.δ Φ.presheafFiber G₁ G₂)]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ, CategoryTheory.cancel_mono, CategoryTheory.GrothendieckTopology.Point.presheafFiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : LocallySmall.{w, v, u} C
inst_5 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_6 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst_7 : MorphismProperty.IsMonoidal (C := Functor.{v, v', u, u'} Cᵒᵖ A) J.W
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : HasProducts.{w, v', u'} A
⊢ NatTrans.IsMonoidal (C := Functor.{v, v', u, u'} Cᵒᵖ A) (F₁ := presheafToSheaf J A ⋙ Φ.sheafFiber)
    (Iso.hom (Φ.presheafToSheafCompSheafFiberIso A))

Tactic:
Localization.Monoidal.lifting_isMonoidal (presheafToSheaf J A) J.W
    Φ.sheafFiber Φ.presheafFiber

Premises used: CategoryTheory.Localization.Monoidal.lifting_isMonoidal, CategoryTheory.presheafToSheaf, CategoryTheory.GrothendieckTopology.W, CategoryTheory.GrothendieckTopology.Point.presheafFiber, CategoryTheory.GrothendieckTopology.Point.sheafFiber
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
J : GrothendieckTopology.{v, u} C
⊢ HasColimitsOfShape.{v', u', w, w + 1} Nᵒᵖ (Type w)

Tactic:
hasColimitsOfShape_of_finallySmall _ _

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
X : C
x : (fiber p).obj X
obtain :
  ∀ (U : Nᵒᵖ) (f : (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj U),
    ∃ (U_1 : N) (f_1 : p.obj U_1 ⟶ X),
      Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f_1)
        ((hom (FC := TypeCat.Fun) ((colimit.cocone (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X)).ι.app U) :
            (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj U)) →
              (fun (X : Type w) ↦ X)
                (((Functor.const Nᵒᵖ).obj (colimit.cocone (p.op ⋙ shrinkYoneda.{w, v, u}.obj X)).pt).obj U))
          f)
⊢ ∃ (U : N) (f : p.obj U ⟶ X), fiberMk f = x

Tactic:
obtain ⟨U, f, rfl⟩ := Types.jointly_surjective_of_isColimit
    (colimit.isColimit (p.op ⋙ shrinkYoneda.{w}.obj X)) x

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
X : C
U : Nᵒᵖ
f : (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj U
obtain :
  ∀ (f : unop (p.op.obj U) ⟶ X),
    ∃ (U_1 : N) (f_1 : p.obj U_1 ⟶ X),
      Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f_1)
        ((hom (FC := TypeCat.Fun) ((colimit.cocone (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X)).ι.app U) :
            (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj U)) →
              (fun (X : Type w) ↦ X)
                (((Functor.const Nᵒᵖ).obj (colimit.cocone (p.op ⋙ shrinkYoneda.{w, v, u}.obj X)).pt).obj U))
          ((Equiv.symm shrinkYonedaObjObjEquiv :
                (a : unop (p.op.obj U) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj U))
              f :
            Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj U)))
⊢ ∃ (U_1 : N) (f_1 : p.obj U_1 ⟶ X),
    Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f_1)
      ((hom (FC := TypeCat.Fun) ((colimit.cocone (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X)).ι.app U) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj U)) →
            (fun (X : Type w) ↦ X)
              (((Functor.const Nᵒᵖ).obj (colimit.cocone (p.op ⋙ shrinkYoneda.{w, v, u}.obj X)).pt).obj U))
        f)

Tactic:
obtain ⟨f, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective f

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
X : C
U : Nᵒᵖ
f : unop (p.op.obj U) ⟶ X
⊢ ∃ (U_1 : N) (f_1 : p.obj U_1 ⟶ X),
    Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f_1)
      ((hom (FC := TypeCat.Fun) ((colimit.cocone (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X)).ι.app U) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj U)) →
            (fun (X : Type w) ↦ X)
              (((Functor.const Nᵒᵖ).obj (colimit.cocone (p.op ⋙ shrinkYoneda.{w, v, u}.obj X)).pt).obj U))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj U) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj U))
            f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj U)))

Tactic:
⟨U.unop, f, rfl⟩

Premises used: Exists.intro, Opposite.unop, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
X : C
U : Nᵒᵖ
f : unop (p.op.obj U) ⟶ X
⊢ ∃ (U_1 : N) (f_1 : p.obj U_1 ⟶ X),
    Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f_1)
      ((hom (FC := TypeCat.Fun) ((colimit.cocone (p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X)).ι.app U) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj U)) →
            (fun (X : Type w) ↦ X)
              (((Functor.const Nᵒᵖ).obj (colimit.cocone (p.op ⋙ shrinkYoneda.{w, v, u}.obj X)).pt).obj U))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj U) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj U))
            f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj U)))

Tactic:
exact ⟨U.unop, f, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
inst_4 : IsCofiltered.{v', u'} N
U : N
X : C
f₁ f₂ : p.obj U ⟶ X
hf : Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f₁) (fiberMk f₂)
obtain :
  ∀ (V : Nᵒᵖ) (g : op U ⟶ V)
    (hg :
      Eq (α := (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
        ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
              (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
                (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
            ((Equiv.symm shrinkYonedaObjObjEquiv :
                  (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
                f₁ :
              Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
          (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
        ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
              (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
                (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
            ((Equiv.symm shrinkYonedaObjObjEquiv :
                  (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
                f₂ :
              Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
          (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))),
    ∃ (V : N) (g : V ⟶ U), p.map g ≫ f₁ = p.map g ≫ f₂
⊢ ∃ (V : N) (g : V ⟶ U), p.map g ≫ f₁ = p.map g ≫ f₂

Tactic:
obtain ⟨V, g, hg⟩ :=
    (Types.FilteredColimit.isColimit_eq_iff'
      (colimit.isColimit (p.op ⋙ shrinkYoneda.{w}.obj X)) _ _).1 hf
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
inst_4 : IsCofiltered.{v', u'} N
U : N
X : C
f₁ f₂ : p.obj U ⟶ X
hf : Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f₁) (fiberMk f₂)
V : Nᵒᵖ
g : op U ⟶ V
hg :
  Eq (α := (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
    ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
            (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
            f₁ :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
      (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
    ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
            (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
            f₂ :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
      (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
⊢ ∃ (V : N) (g : V ⟶ U), p.map g ≫ f₁ = p.map g ≫ f₂

Tactic:
⟨V.unop, g.unop, ?_⟩

Premises used: Quiver.Hom.unop, Exists.intro, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
N : Type u'
inst_2 : Category.{v', u'} N
p : Functor.{v', v, u', u} N C
inst_3 : InitiallySmall.{w, v', u'} N
inst_4 : IsCofiltered.{v', u'} N
U : N
X : C
f₁ f₂ : p.obj U ⟶ X
hf : Eq.{w + 1} (α := (fiber p).obj X) (fiberMk f₁) (fiberMk f₂)
V : Nᵒᵖ
g : op U ⟶ V
hg :
  Eq (α := (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
    ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
            (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
            f₁ :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
      (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
    ((hom (FC := TypeCat.Fun) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).map g) :
          (a : (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj (op U))) →
            (fun (X : Type w) ↦ X) ((p.op ⋙ shrinkYoneda.{w, v, u}.obj X).obj V))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
              (a : unop (p.op.obj (op U)) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (p.op.obj (op U)))
            f₂ :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (p.op.obj (op U))) :
      (fun (X : Type w) ↦ X) ((p.op ⋙ Functor.obj shrinkYoneda.{w, v, u} X).obj V))
refine : p.map g.unop ≫ f₁ = p.map g.unop ≫ f₂
⊢ ∃ (V : N) (g : V ⟶ U), p.map g ≫ f₁ = p.map g ≫ f₂

Tactic:
refine ⟨V.unop, g.unop, ?_⟩