-- Module: Mathlib.CategoryTheory.Sites.Preserves
Goal:
C : Type u
inst : Category.{v, u} C
I : C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
hF :
  IsSheafFor (X := I) F
    (ofArrows Empty.elim fun (a : Empty) ↦ Empty.instIsEmpty.elim (p := fun (x : Empty) ↦ x.elim ⟶ I) a)
hI : IsInitial.{v, u} I
α : Type u_1
inst_1 : Small.{w, u_1} α
X : α → C
c : Cofan.{u_1, v, u} X
inst_2 : (ofArrows X c.inj).HasPairwisePullbacks
inst_3 : HasInitial.{v, u} C
inst_4 : ∀ (i : α), Mono (c.inj i)
hd :
  Pairwise fun (i j : α) ↦ IsPullback (P := initial.{v, u} C) (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)
i j : α
a : Equalizer.Presieve.Arrows.FirstObj F X
h :
  Eq (α := F.obj (op (pullback (c.inj i) (c.inj j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.fst (c.inj i) (c.inj j)))) :
          (a : F.obj (op (X i))) → F.obj (op (pullback (c.inj i) (c.inj j))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : α) ↦ F.obj (op (X i))) i) :
              (a : Equalizer.Presieve.Arrows.FirstObj F X) → F.obj (op (X i)))
            a :
          F.obj (op (X i))) :
      F.obj (op (pullback (c.inj i) (c.inj j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (pullback.snd (c.inj i) (c.inj j)))) :
          (a : F.obj (op (X j))) → F.obj (op (pullback (c.inj i) (c.inj j))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π (fun (i : α) ↦ F.obj (op (X i))) j) :
              (a : Equalizer.Presieve.Arrows.FirstObj F X) → F.obj (op (X j)))
            a :
          F.obj (op (X j))) :
      F.obj (op (pullback (c.inj i) (c.inj j))))
⊢ Eq (α := F.obj (op (pullback (X := X (i, j).1) (Y := X (i, j).2) (c.inj (i, j).1) (c.inj (i, j).2))))
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y :=
            ∏ᶜ fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
            (Equalizer.Presieve.Arrows.firstMap F X c.inj :
              Equalizer.Presieve.Arrows.FirstObj F X ⟶ Equalizer.Presieve.Arrows.SecondObj F X c.inj)
            (Pi.π (fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
              (i, j))))
        a :
      F.obj (op (pullback (X := X (i, j).1) (Y := X (i, j).2) (c.inj (i, j).1) (c.inj (i, j).2))))
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y :=
            ∏ᶜ fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
            (Equalizer.Presieve.Arrows.secondMap F X c.inj :
              Equalizer.Presieve.Arrows.FirstObj F X ⟶ Equalizer.Presieve.Arrows.SecondObj F X c.inj)
            (Pi.π (fun (ij : α × α) ↦ F.obj (op (pullback (X := X ij.1) (Y := X ij.2) (c.inj ij.1) (c.inj ij.2))))
              (i, j))))
        a :
      F.obj (op (pullback (X := X (i, j).1) (Y := X (i, j).2) (c.inj (i, j).1) (c.inj (i, j).2))))

Tactic:
simp only [Equalizer.Presieve.Arrows.firstMap, limit.lift_π, Fan.mk_pt, Fan.mk_π_app,
    TypeCat.Fun.toFun_apply, comp_apply, Equalizer.Presieve.Arrows.secondMap]

Premises used: TypeCat.Fun.toFun_apply, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.comp_apply, CategoryTheory.Equalizer.Presieve.Arrows.firstMap, CategoryTheory.Equalizer.Presieve.Arrows.secondMap, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app