-- 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
V 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φ₂
have refine_2 : ∀ (W : N) (g : W ⟶ V) (hg : p.map g ≫ φ₁ = p.map g ≫ φ₂),
  ∃ (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 ⟨W, g, hg⟩ := exists_of_fiberMk_eq_fiberMk
      (show fiberMk.{w} φ₁ = fiberMk.{w} φ₂ by simpa using hφ₁.trans hφ₂.symm)