awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))))

Tactic:
⟨X, x, z, rfl⟩

Premises used: Exists.intro, rfl
-- 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
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))))

Tactic:
exact ⟨X, x, z, rfl⟩
-- 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
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
⊢ Eq (α := CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
            (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
          z₁ :
        CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
            (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
          z₂ :
        CC (Functor.obj Φ.presheafFiber P)) ↔
    ∃ (Y : C) (f : Y ⟶ X) (y : Φ.fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
            y =
          x ∧
        Eq (α := CC (P.obj (op Y)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₁ :
            CC (P.obj (op Y)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₂ :
            CC (P.obj (op Y)))

Tactic:
((colimit.isColimit ((CategoryOfElements.π Φ.fiber).op ⋙ P)).eq_iff' ..).trans ?_

Premises used: CategoryTheory.Functor.op, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.CategoryOfElements.π, CategoryTheory.Limits.colimit, Iff.trans, CategoryTheory.Limits.IsColimit.eq_iff', CategoryTheory.GrothendieckTopology.Point.fiber, 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
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
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
Y : C
f : Y ⟶ X
y : Φ.fiber.obj Y
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      y =
    x
hf' :
  Eq (α := CC (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₁ :
      CC (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₂ :
      CC (P.obj (op Y)))
⊢ ∃ (j : Φ.fiber.Elementsᵒᵖ) (f : op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x) ⟶ j),
    Eq (α := CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
            (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
              CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
          z₁ :
        CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
            (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
              CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
          z₂ :
        CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))

Tactic:
⟨⟨Y, y⟩, ⟨f, hf⟩, hf'⟩

Premises used: Subtype.mk, Opposite.op, Exists.intro, Sigma.mk
-- 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
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
Y : C
f : Y ⟶ X
y : Φ.fiber.obj Y
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      y =
    x
hf' :
  Eq (α := CC (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₁ :
      CC (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₂ :
      CC (P.obj (op Y)))
⊢ ∃ (j : Φ.fiber.Elementsᵒᵖ) (f : op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x) ⟶ j),
    Eq (α := CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
            (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
              CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
          z₁ :
        CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
            (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
              CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
          z₂ :
        CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))

Tactic:
exact ⟨⟨Y, y⟩, ⟨f, hf⟩, hf'⟩
-- 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 Q : 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
f : P ⟶ Q
inst_7 : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
p : CC (Functor.obj Φ.presheafFiber Q)
obtain :
  ∀ (X : C) (x : Φ.fiber.obj X) (z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Q.obj (op X))),
    ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
      Eq (α := CC (Functor.obj Φ.presheafFiber Q))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
              (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
            a :
          CC (Functor.obj Φ.presheafFiber Q))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x Q) :
              (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
            z :
          CC (Functor.obj Φ.presheafFiber Q))
⊢ ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
          (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
        a =
      p

Tactic:
obtain ⟨X, x, z, rfl⟩ := Φ.toPresheafFiber_jointly_surjective p

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_jointly_surjective, rfl
-- 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 Q : 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
f : P ⟶ Q
inst_7 : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
X : C
x : Φ.fiber.obj X
z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Q.obj (op X))
obtain :
  ∀ (Y : C) (g : Y ⟶ unop (op X)) (t : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op Y)))
    (ht :
      Eq (α := CC (Q.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op Y)) : (a : CC (P.obj (op Y))) → CC (Q.obj (op Y))) t :
          CC (Q.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map g.op) :
              (a : CC (Q.obj (op (unop (op X))))) → CC (Q.obj (op Y)))
            z :
          CC (Q.obj (op Y))))
    (y : Φ.fiber.obj Y),
    ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
      Eq (α := CC (Functor.obj Φ.presheafFiber Q))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
              (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
            a :
          CC (Functor.obj Φ.presheafFiber Q))
        ((ConcreteCategory.hom (FC := FC) (CC := CC)
                (Φ.toPresheafFiber X
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                      (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op X))))
                    y)
                  Q) :
              (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
            z :
          CC (Functor.obj Φ.presheafFiber Q))
⊢ ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
    Eq (α := CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
            (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
          a :
        CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x Q) :
            (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
          z :
        CC (Functor.obj Φ.presheafFiber Q))

Tactic:
obtain ⟨Y, g, ⟨t, ht⟩, y, rfl⟩ := Φ.jointly_surjective _ (Presheaf.imageSieve_mem J f z) x

Premises used: CategoryTheory.GrothendieckTopology.Point.jointly_surjective, CategoryTheory.Presheaf.imageSieve_mem, rfl
-- 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 Q : 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
f : P ⟶ Q
inst_7 : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
X : C
z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Q.obj (op X))
Y : C
g : Y ⟶ unop (op X)
t : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op Y))
ht :
  Eq (α := CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op Y)) : (a : CC (P.obj (op Y))) → CC (Q.obj (op Y))) t :
      CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map g.op) : (a : CC (Q.obj (op (unop (op X))))) → CC (Q.obj (op Y)))
        z :
      CC (Q.obj (op Y)))
y : Φ.fiber.obj Y
⊢ Eq (α := CC (Functor.obj Φ.presheafFiber Q))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
          (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber Y y P) :
              (a : CC (P.obj (op Y))) → CC (Φ.presheafFiber.obj P))
            t :
          CC (Functor.obj Φ.presheafFiber P)) :
      CC (Functor.obj Φ.presheafFiber Q))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (Φ.toPresheafFiber X
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                  (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op X))))
                y)
              Q) :
          (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
        z :
      CC (Functor.obj Φ.presheafFiber Q))

Tactic:
simp [← toPresheafFiber_w, ← ht]

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w
-- 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 Q : 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
f : P ⟶ Q
inst_7 : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
X : C
z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Q.obj (op X))
Y : C
g : Y ⟶ unop (op X)
t : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op Y))
ht :
  Eq (α := CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op Y)) : (a : CC (P.obj (op Y))) → CC (Q.obj (op Y))) t :
      CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map g.op) : (a : CC (Q.obj (op (unop (op X))))) → CC (Q.obj (op Y)))
        z :
      CC (Q.obj (op Y)))
y : Φ.fiber.obj Y
⊢ ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
    Eq (α := CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
            (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
          a :
        CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (Φ.toPresheafFiber X
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                    (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op X))))
                  y)
                Q) :
            (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
          z :
        CC (Functor.obj Φ.presheafFiber Q))

Tactic:
exact ⟨Φ.toPresheafFiber Y y P t, by simp [← toPresheafFiber_w, ← ht]⟩
-- 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 Q : 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
f : P ⟶ Q
inst_7 : Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f
this :
  ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X)))
    (hp :
      Eq (α := CC (Q.obj (op X)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₁ :
          CC (Q.obj (op X)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₂ :
          CC (Q.obj (op X)))),
    Eq (α := CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
            (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
          p₁ :
        CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
            (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
          p₂ :
        CC (Functor.obj Φ.presheafFiber P))
X : C
p₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
Y : C
g : Y ⟶ X
y : Φ.fiber.obj Y
h :
  Eq (α := CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map g.op) : (a : CC (Q.obj (op X))) → CC (Q.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₁ :
          CC (Q.obj (op X))) :
      CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map g.op) : (a : CC (Q.obj (op X))) → CC (Q.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₂ :
          CC (Q.obj (op X))) :
      CC (Q.obj (op Y)))
⊢ Eq (α := CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op Y)) : (a : CC (P.obj (op Y))) → CC (Q.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map g.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) p₁ :
          CC (P.obj (op Y))) :
      CC (Q.obj (op Y)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op Y)) : (a : CC (P.obj (op Y))) → CC (Q.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map g.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) p₂ :
          CC (P.obj (op Y))) :
      CC (Q.obj (op Y)))

Tactic:
simp only [← NatTrans.naturality_apply] at h

Premises used: CategoryTheory.NatTrans.naturality_apply