-- 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
inst_4 : IsCofiltered.{v', u'} N
X : C
x : (fiber p).obj X
V : N
φ₁ :
  Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).fst (β := fun (c : C) ↦ (fiber p).obj c)
hφ₁ :
  (hom (FC := TypeCat.Fun) ((fiber p).map φ₁) :
        (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
          (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, x⟩.fst))
      (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) =
    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).snd (β := fun (c : C) ↦ (fiber p).obj c)
φ₂ :
  Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).fst (β := fun (c : C) ↦ (fiber p).obj c)
hφ₂ :
  (hom (FC := TypeCat.Fun) ((fiber p).map φ₂) :
        (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
          (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, x⟩.fst))
      (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) =
    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).snd (β := fun (c : C) ↦ (fiber p).obj c)
refine_2 :
  ∀ (U : N) (f : p.obj U ⟶ X)
    (φ₁ :
      Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
        Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))
    (hφ₁ :
      Eq (α :=
        (fun (X : Type w) ↦ X)
          ((fiber p).obj
            (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
              (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
        ((hom (FC := TypeCat.Fun) ((fiber p).map φ₁) :
              (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
                (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, fiberMk f⟩.fst))
            (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) :
          (fun (X : Type w) ↦ X)
            ((fiber p).obj
              (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
        (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)) :
          (fiber p).obj
            (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
              (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
    (φ₂ :
      Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
        Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))
    (hφ₂ :
      Eq (α :=
        (fun (X : Type w) ↦ X)
          ((fiber p).obj
            (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
              (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
        ((hom (FC := TypeCat.Fun) ((fiber p).map φ₂) :
              (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
                (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, fiberMk f⟩.fst))
            (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) :
          (fun (X : Type w) ↦ X)
            ((fiber p).obj
              (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
        (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)) :
          (fiber p).obj
            (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
              (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))))),
    ∃ (c' : N) (t : c' ⟶ V),
      Functor.map (functor p) t ≫
          Subtype.mk (p :=
            fun
              (f_1 :
                Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
                  Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))) ↦
            Eq (α :=
              (fun (X : Type w) ↦ X)
                ((fiber p).obj
                  (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
              ((hom (FC := TypeCat.Fun) ((fiber p).map f_1) :
                    (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
                      (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, fiberMk f⟩.fst))
                  (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) :
                (fun (X : Type w) ↦ X)
                  ((fiber p).obj
                    (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                      (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
              (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c)
                  (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)) :
                (fiber p).obj
                  (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
            φ₁ hφ₁ =
        Functor.map (functor p) t ≫
          Subtype.mk (p :=
            fun
              (f_1 :
                Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
                  Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f))) ↦
            Eq (α :=
              (fun (X : Type w) ↦ X)
                ((fiber p).obj
                  (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
              ((hom (FC := TypeCat.Fun) ((fiber p).map f_1) :
                    (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
                      (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, fiberMk f⟩.fst))
                  (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) :
                (fun (X : Type w) ↦ X)
                  ((fiber p).obj
                    (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                      (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
              (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c)
                  (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)) :
                (fiber p).obj
                  (Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c)
                    (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X (fiberMk f)))))
            φ₂ hφ₂
⊢ ∃ (c' : N) (t : c' ⟶ V),
    Functor.map (functor p) t ≫
        Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
                (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).fst (β := fun (c : C) ↦ (fiber p).obj c)) ↦
          (hom (FC := TypeCat.Fun) ((fiber p).map f) :
                (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
                  (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, x⟩.fst))
              (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) =
            (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).snd (β := fun (c : C) ↦ (fiber p).obj c))
          φ₁ hφ₁ =
      Functor.map (functor p) t ≫
        Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V) ⟶
                (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).fst (β := fun (c : C) ↦ (fiber p).obj c)) ↦
          (hom (FC := TypeCat.Fun) ((fiber p).map f) :
                (a : (fun (X : Type w) ↦ X) ((fiber p).obj ((functor p).obj V).fst)) →
                  (fun (X : Type w) ↦ X) ((fiber p).obj ⟨X, x⟩.fst))
              (Sigma.snd (β := fun (c : C) ↦ (fiber p).obj c) (Functor.obj (functor p) V)) =
            (Sigma.mk (β := fun (c : C) ↦ (fiber p).obj c) X x).snd (β := fun (c : C) ↦ (fiber p).obj c))
          φ₂ hφ₂

Tactic:
obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x

Premises used: CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_jointly_surjective, rfl