awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
hγ : CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (J.plusLift γ hR) = η ≫ γ
hγ₁ : CategoryStruct.comp (Y := J.plusObj Q) (η ≫ J.toPlus Q) (J.plusLift γ hR) = η ≫ γ
hγ₂ : η ≫ CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus Q) (J.plusLift γ hR) = η ≫ γ
hγ₃ hγ₄ : η ≫ γ = η ≫ γ
⊢ CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (J.plusMap η ≫ J.plusLift γ hR) = η ≫ γ

Tactic:
rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.toPlus_naturality, CategoryTheory.GrothendieckTopology.toPlus_plusLift
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
w :
  ∀ (x : Cᵒᵖ),
    Eq.{w' + 1} (α := (Functor.obj (J.plusFunctor D) F).obj x ⟶ (Functor.obj (J.plusFunctor D) G).obj x)
      (NatTrans.app (Functor.map (J.plusFunctor D) 0) x) (NatTrans.app 0 x)
⊢ Eq (α := Functor.obj (J.plusFunctor D) F ⟶ Functor.obj (J.plusFunctor D) G) (Functor.map (J.plusFunctor D) 0) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
w : Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app (J.plusMap 0) x) 0
⊢ Eq.{w' + 1} (α := (Functor.obj (J.plusFunctor D) F).obj x ⟶ (Functor.obj (J.plusFunctor D) G).obj x)
    (NatTrans.app (Functor.map (J.plusFunctor D) 0) x) (NatTrans.app 0 x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Plus
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
w : Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app 0 x) 0
w₁ w₂ : Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) 0 0
⊢ Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app (J.plusMap 0) x) 0

Tactic:
rw [J.plusMap_zero, NatTrans.app_zero]

Premises used: CategoryTheory.NatTrans.app_zero, CategoryTheory.GrothendieckTopology.plusMap_zero
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
⊢ HasColimitsOfShape Φ.fiber.Elementsᵒᵖ A

Tactic:
hasColimitsOfShape_of_finallySmall _ _

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
⊢ IsSifted Φ.fiber.Elementsᵒᵖ

Tactic:
IsFiltered.isSifted

Premises used: CategoryTheory.IsFiltered.isSifted
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
inst_5 : LocallySmall.{w, v, u} C
inst_6 : AB5OfSize.{w, w, v', u'} A
inst_7 : HasFiniteLimits.{v', u'} A
⊢ HasExactColimitsOfShape Φ.fiber.Elementsᵒᵖ A

Tactic:
hasExactColimitsOfShape_of_final _
    (FinallySmall.fromFilteredFinalModel Φ.fiber.Elementsᵒᵖ)

Premises used: CategoryTheory.Functor.Elements, Opposite, CategoryTheory.hasExactColimitsOfShape_of_final, CategoryTheory.FinallySmall.fromFilteredFinalModel, CategoryTheory.GrothendieckTopology.Point.fiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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 : HasColimitsOfSize.{w, w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
T : A
f g : Functor.obj Φ.presheafFiber P ⟶ T
h : ∀ (X : C) (x : Φ.fiber.obj X), Φ.toPresheafFiber X x P ≫ f = Φ.toPresheafFiber X x P ≫ g
X : C
x : Φ.fiber.obj X
⊢ Eq (α :=
    (Functor.obj (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op)
            P).obj
        (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x)) ⟶
      T)
    (colimit.ι
        (Functor.obj (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op)
          P)
        (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x)) ≫
      f)
    (colimit.ι
        (Functor.obj (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op)
          P)
        (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x)) ≫
      g)

Tactic:
h X x

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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 : HasColimitsOfSize.{w, w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
T : A
f g : Functor.obj Φ.presheafFiber P ⟶ T
h : ∀ (X : C) (x : Φ.fiber.obj X), Φ.toPresheafFiber X x P ≫ f = Φ.toPresheafFiber X x P ≫ g
X : C
x : Φ.fiber.obj X
⊢ Eq (α :=
    (Functor.obj (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op)
            P).obj
        (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x)) ⟶
      T)
    (colimit.ι
        (Functor.obj (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op)
          P)
        (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x)) ≫
      f)
    (colimit.ι
        (Functor.obj (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op)
          P)
        (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x)) ≫
      g)

Tactic:
exact h X x
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
X : C
x : Φ.fiber.obj X
x_1 x_2 : Functor.{v, v', u, u'} Cᵒᵖ A
f : x_1 ⟶ x_2
⊢ Eq (α := Functor.obj (Functor.obj (evaluation Cᵒᵖ A) (op X)) x_1 ⟶ Functor.obj Φ.presheafFiber x_2)
    (Functor.map (Functor.obj (evaluation Cᵒᵖ A) (op X)) f ≫ Φ.toPresheafFiber X x x_2)
    (Φ.toPresheafFiber X x x_1 ≫ Functor.map Φ.presheafFiber f)

Tactic:
simp [presheafFiber, toPresheafFiber]

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.GrothendieckTopology.Point.presheafFiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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 : HasColimitsOfSize.{w, w, v', u'} A
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
P : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ Eq (α := P.obj (op Y) ⟶ Functor.obj Φ.presheafFiber P) (P.map f.op ≫ Φ.toPresheafFiber X x P)
    (Φ.toPresheafFiber Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj X)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y))
        x)
      P)

Tactic:
colimit.w ((CategoryOfElements.π Φ.fiber).op ⋙ P)
      (CategoryOfElements.homMk ⟨X, x⟩ ⟨Y, Φ.fiber.map f x⟩ f rfl).op

Premises used: CategoryTheory.Functor.op, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.comp, CategoryTheory.CategoryOfElements.homMk, CategoryTheory.CategoryOfElements.π, CategoryTheory.Limits.colimit, CategoryTheory.Functor.map, Sigma.mk, CategoryTheory.Limits.colimit.w, DFunLike.coe, rfl, CategoryTheory.GrothendieckTopology.Point.fiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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 : HasColimitsOfSize.{w, w, v', u'} A
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
g : P ⟶ Q
X : C
x : Φ.fiber.obj X
⊢ Eq (α := P.obj (op X) ⟶ Functor.obj Φ.presheafFiber Q) (Φ.toPresheafFiber X x P ≫ Functor.map Φ.presheafFiber g)
    (g.app (op X) ≫ Φ.toPresheafFiber X x Q)

Tactic:
((Φ.toPresheafFiberNatTrans X x).naturality g).symm

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
⊢ Eq (α := (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u} ⋙ Φ.presheafFiber).obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.inv Φ.shrinkYonedaCompPresheafFiberIso) X) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj X)) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u} ⋙ Φ.presheafFiber).obj X))
        x :
      (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u} ⋙ Φ.presheafFiber).obj X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} X)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
            (𝟙 X) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X)))

Tactic:
Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply
    _ (Functor.elementsMk (Φ.fiber) _ x)

Premises used: CategoryTheory.Functor.elementsMk, CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply, CategoryTheory.GrothendieckTopology.Point.fiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
⊢ Eq (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.presheafFiber (Functor.map shrinkYoneda.{w, v, u} f)) :
          (a : (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} X)) :
              (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X)))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
                (𝟙 X) :
              Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
          (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj Y).obj (op X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))

Tactic:
(Φ.toPresheafFiber_naturality_apply (shrinkYoneda.{w}.map f) _ x
    (shrinkYonedaObjObjEquiv.symm (𝟙 X))).trans (congr_arg _ ?_)

Premises used: CategoryTheory.shrinkYoneda, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality_apply, CategoryTheory.Functor.map, congr_arg, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
refine :
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} f) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj X).obj (op X)) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
            (𝟙 X) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
⊢ Eq (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.presheafFiber (Functor.map shrinkYoneda.{w, v, u} f)) :
          (a : (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} X)) :
              (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X)))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
                (𝟙 X) :
              Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
          (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj Y).obj (op X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))

Tactic:
refine (Φ.toPresheafFiber_naturality_apply (shrinkYoneda.{w}.map f) _ x
    (shrinkYonedaObjObjEquiv.symm (𝟙 X))).trans (congr_arg _ ?_)
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
⊢ Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} f) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj X).obj (op X)) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
            (𝟙 X) :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))

Tactic:
simpa using shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w} (𝟙 _) f
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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 : HasColimitsOfSize.{w, w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
T : A
φ : (X : C) → Φ.fiber.obj X → (P.obj (op X) ⟶ T)
hφ :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
    P.map f.op ≫ φ X x =
      φ Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj X)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y))
          x)
X : C
x : Φ.fiber.obj X
⊢ CategoryStruct.comp (Y := Functor.obj Φ.presheafFiber P) (Φ.toPresheafFiber X x P) (Φ.presheafFiberDesc φ hφ) = φ X x

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
FC : A → A → Type u_1
CC : A → Type w'
inst_5 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
inst_7 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_8 : LocallySmall.{w, v, u} C
⊢ PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ (forget A (FC := FC) (CC := CC))

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

Premises used: CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final, CategoryTheory.FinallySmall.fromFilteredFinalModel
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
p : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Functor.obj Φ.presheafFiber P)
obtain :
  ∀ (X : C) (x : Φ.fiber.obj X)
    (z :
      (((CategoryOfElements.π Φ.fiber).op ⋙ P) ⋙ forget A (FC := FC) (CC := CC)).obj
        (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))),
    ∃ (X_1 : C) (x_1 : Φ.fiber.obj X_1) (z_1 : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X_1))),
      Eq (α := CC (Functor.obj Φ.presheafFiber P))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X_1 x_1 P) :
              (a : CC (P.obj (op X_1))) → CC (Φ.presheafFiber.obj P))
            z_1 :
          CC (Functor.obj Φ.presheafFiber P))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cocone.ι
                    (Functor.mapCocone (forget A (FC := FC) (CC := CC))
                      (colimit.cocone ((CategoryOfElements.π Φ.fiber).op ⋙ P))))
                  (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))) :
              (a : (fun (X : Type w') ↦ X) ((((CategoryOfElements.π Φ.fiber).op ⋙ P) ⋙ forget A).obj (op ⟨X, x⟩))) →
                (fun (X : Type w') ↦ X)
                  (((Functor.const Φ.fiber.Elementsᵒᵖ).obj
                        ((forget A).mapCocone (colimit.cocone ((CategoryOfElements.π Φ.fiber).op ⋙ P))).pt).obj
                    (op ⟨X, x⟩)))
            z :
          (fun (X : Type w') ↦ X)
            (Functor.obj
              (Functor.obj (Functor.const Φ.fiber.Elementsᵒᵖ)
                (Cocone.pt (F := ((CategoryOfElements.π Φ.fiber).op ⋙ P) ⋙ forget A (FC := FC) (CC := CC))
                  (Functor.mapCocone (forget A (FC := FC) (CC := CC))
                    (colimit.cocone ((CategoryOfElements.π Φ.fiber).op ⋙ P)))))
              (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))))
⊢ ∃ (X : C) (x : Φ.fiber.obj X) (z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        z =
      p

Tactic:
obtain ⟨⟨X, x⟩, z, rfl⟩ := Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget A)
      (colimit.isColimit ((CategoryOfElements.π Φ.fiber).op ⋙ P))) p

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.CategoryOfElements.π, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves, rfl, CategoryTheory.GrothendieckTopology.Point.fiber