-- 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
x : I × I
ij : P.obj (op B)
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))))
⊢ 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))))

Tactic:
dsimp [forkMap, firstMap, secondMap]

Premises used: CategoryTheory.Equalizer.Presieve.Arrows.forkMap, CategoryTheory.Equalizer.Presieve.Arrows.firstMap, CategoryTheory.Equalizer.Presieve.Arrows.secondMap