-- 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
x : I × I
ij : P.obj (op B)
⊢ Eq (α := P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y :=
            ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
            (forkMap P X π ≫ firstMap P X π : P.obj (op B) ⟶ SecondObj P X π)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x)))
        ij :
      P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y :=
            ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2))))
            (forkMap P X π ≫ secondMap P X π : P.obj (op B) ⟶ SecondObj P X π)
            (Pi.π (fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) x)))
        ij :
      P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
have h : Eq (α := P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.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)))) x) :
        (a : ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) →
          P.obj (op (Limits.pullback (π x.1) (π x.2))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.lift (f := fun (ij : I × I) ↦
                P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) fun (x : I × I) ↦
                Pi.π (fun (i : I) ↦ P.obj (op (X i))) x.1 ≫ P.map (Quiver.Hom.op (pullback.fst (π x.1) (π x.2)))) :
            (a : FirstObj P X) → ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Pi.lift (f := fun (i : I) ↦ P.obj (op (X i))) fun (i : I) ↦ P.map (π i).op) :
                (a : P.obj (op B)) → FirstObj P X)
              ij :
            FirstObj P X) :
        ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) :
    P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.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)))) x) :
        (a : ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) →
          P.obj (op (Limits.pullback (π x.1) (π x.2))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.lift (f := fun (ij : I × I) ↦
                P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) fun (x : I × I) ↦
                Pi.π (fun (i : I) ↦ P.obj (op (X i))) x.2 ≫ P.map (Quiver.Hom.op (pullback.snd (π x.1) (π x.2)))) :
            (a : FirstObj P X) → ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Pi.lift (f := fun (i : I) ↦ P.obj (op (X i))) fun (i : I) ↦ P.map (π i).op) :
                (a : P.obj (op B)) → FirstObj P X)
              ij :
            FirstObj P X) :
        ∏ᶜ fun (ij : I × I) ↦ P.obj (op (Limits.pullback (X := X ij.1) (Y := X ij.2) (π ij.1) (π ij.2)))) :
    P.obj (op (Limits.pullback (X := X x.1) (Y := X x.2) (π x.1) (π x.2))))
Tactic: dsimp [forkMap, firstMap, secondMap]