-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
                ij) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))
          z₁ :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
                ij) :
            (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))
          z₂ :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))))
w :
  ∀ (j : Discrete (I × I)),
    Eq (α :=
      (fun (X : Type w) ↦ X)
        (Functor.obj
          (Discrete.functor fun (ij : I × I) ↦
            P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
          j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (limit.π
                (Discrete.functor fun (ij : I × I) ↦
                  P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
                j) :
            (a :
                (fun (X : Type w) ↦ X)
                  (limit (Discrete.functor fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))) →
              (fun (X : Type w) ↦ X)
                ((Discrete.functor fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))).obj j))
          z₁ :
        (fun (X : Type w) ↦ X)
          (Functor.obj
            (Discrete.functor fun (ij : I × I) ↦
              P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (limit.π
                (Discrete.functor fun (ij : I × I) ↦
                  P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
                j) :
            (a :
                (fun (X : Type w) ↦ X)
                  (limit (Discrete.functor fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))))) →
              (fun (X : Type w) ↦ X)
                ((Discrete.functor fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))).obj j))
          z₂ :
        (fun (X : Type w) ↦ X)
          (Functor.obj
            (Discrete.functor fun (ij : I × I) ↦
              P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
            j))
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Premises used: CategoryTheory.Limits.Types.limit_ext