-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve.{v, u} X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    Eq (α :=
      (fun (X : Type (max u v)) ↦ X)
        (P.obj
          (op
            (Sigma.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })
              (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π
                (fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                  P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))) :
            (a : (fun (X : Type (max u v)) ↦ X) (∏ᶜ fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst))) →
              (fun (X : Type (max u v)) ↦ X) (P.obj (op ⟨Y, ⟨f, hf⟩⟩.fst)))
          z₁ :
        (fun (X : Type (max u v)) ↦ X)
          (P.obj
            (op
              (Sigma.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y
                  (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π
                (fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                  P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))) :
            (a : (fun (X : Type (max u v)) ↦ X) (∏ᶜ fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst))) →
              (fun (X : Type (max u v)) ↦ X) (P.obj (op ⟨Y, ⟨f, hf⟩⟩.fst)))
          z₂ :
        (fun (X : Type (max u v)) ↦ X)
          (P.obj
            (op
              (Sigma.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y
                  (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))))))
w :
  ∀ (j : Discrete ((Y : C) × { f : Y ⟶ X // R f })),
    Eq (α :=
      (fun (X : Type (max u v)) ↦ X)
        (Functor.obj
          (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
            P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
          j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (limit.π
                (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                  P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                j) :
            (a :
                (fun (X : Type (max u v)) ↦ X)
                  (limit (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)))) →
              (fun (X : Type (max u v)) ↦ X)
                ((Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)).obj j))
          z₁ :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
              P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (limit.π
                (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                  P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                j) :
            (a :
                (fun (X : Type (max u v)) ↦ X)
                  (limit (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)))) →
              (fun (X : Type (max u v)) ↦ X)
                ((Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)).obj j))
          z₂ :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
              P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
            j))
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Premises used: CategoryTheory.Limits.Types.limit_ext