-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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)))))
⊢ z₁ = z₂
have 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))
Tactic: apply Limits.Types.limit_ext