-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst_1 : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
t :
  Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
          (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
        x :
      (fun (X : Type w) ↦ X) (SecondObj P X π))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
          (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
        x :
      (fun (X : Type w) ↦ X) (SecondObj P X π))
i j : I
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (π i) (π j)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
              (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
            x i :
          P.obj (op (X i))) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (π i) (π j)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) →
            (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.productIso fun (i : I) ↦ P.obj (op (X i)))) :
              (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                (fun (X : Type w) ↦ X) ((j : I) → P.obj (op (X j))))
            x j :
          P.obj (op (X j))) :
      (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
have t₁ : Eq (α :=
  (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).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))))
            (i, j)) :
        (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 (π (i, j).1) (π (i, j).2)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π)) :
    (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).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))))
            (i, j)) :
        (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 (π (i, j).1) (π (i, j).2)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π)) :
    (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (X := X (i, j).1) (Y := X (i, j).2) (π (i, j).1) (π (i, j).2)))))
Tactic: apply_fun Pi.π (fun (ij : I × I) ↦ P.obj (op (pullback (π ij.1) (π ij.2)))) ⟨i, j⟩ at t
Cleared hypotheses: t