-- 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₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Functor.obj Φ.presheafFiber P)
obtain :
  ∀ (X : C) (x : Φ.fiber.obj X)
    (z₁ 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))) (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)))) ∧
        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))) (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₁ ∧
      (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₁, z₂, rfl, rfl⟩ := Types.FilteredColimit.jointly_surjective_of_isColimit₂
    (isColimitOfPreserves (forget A)
      (colimit.isColimit ((CategoryOfElements.π Φ.fiber).op ⋙ P))) p₁ p₂

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