-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered (goal)
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)
⊢ ∃ (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φ₂
have 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φ₂
Tactic: obtain ⟨U, f, rfl⟩ := fiberMk_jointly_surjective x
Cleared hypotheses: x, φ₁, hφ₁, φ₂, hφ₂