-- 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
hi : ¬i = j
this : PreservesLimit (Functor.empty Cᵒᵖ) F
neg :
  ∀ (i_1 : PEmpty.{1}),
    Eq (α := (fun (X : Type w) ↦ X) (Functor.obj (Functor.empty (Type w)) { as := i_1 : Discrete PEmpty.{1} }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (limit.π (Functor.empty (Type w)) { as := i_1 : Discrete PEmpty.{1} }) :
            (a : (fun (X : Type w) ↦ X) (limit (Functor.empty (Type w)))) →
              (fun (X : Type w) ↦ X) ((Functor.empty (Type w)).obj { as := i_1 }))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.hom
                    (F.mapIso (Iso.op (IsPullback.isoPullback ⋯)) ≪≫
                      Iso.trans (Y := F.obj (terminal.{v, u} Cᵒᵖ))
                        (F.mapIso (Iso.symm (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial))))
                        (PreservesTerminal.iso F))) :
                (a : (fun (X : Type w) ↦ X) (F.obj (op (pullback (c.inj i) (c.inj j))))) →
                  (fun (X : Type w) ↦ X) (⊤_ Type w))
              ((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)))) :
            (fun (X : Type w) ↦ X) (⊤_ Type w)) :
        (fun (X : Type w) ↦ X) (Functor.obj (Functor.empty (Type w)) { as := i_1 : Discrete PEmpty.{1} }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (limit.π (Functor.empty (Type w)) { as := i_1 : Discrete PEmpty.{1} }) :
            (a : (fun (X : Type w) ↦ X) (limit (Functor.empty (Type w)))) →
              (fun (X : Type w) ↦ X) ((Functor.empty (Type w)).obj { as := i_1 }))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.hom
                    (F.mapIso (Iso.op (IsPullback.isoPullback ⋯)) ≪≫
                      Iso.trans (Y := F.obj (terminal.{v, u} Cᵒᵖ))
                        (F.mapIso (Iso.symm (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial))))
                        (PreservesTerminal.iso F))) :
                (a : (fun (X : Type w) ↦ X) (F.obj (op (pullback (c.inj i) (c.inj j))))) →
                  (fun (X : Type w) ↦ X) (⊤_ Type w))
              ((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)))) :
            (fun (X : Type w) ↦ X) (⊤_ Type w)) :
        (fun (X : Type w) ↦ X) (Functor.obj (Functor.empty (Type w)) { as := i_1 : Discrete PEmpty.{1} }))
⊢ Eq (α := (fun (X : Type w) ↦ X) (⊤_ Type w))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
              (F.mapIso (Iso.op (IsPullback.isoPullback ⋯)) ≪≫
                Iso.trans (Y := F.obj (terminal.{v, u} Cᵒᵖ))
                  (F.mapIso (Iso.symm (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial))))
                  (PreservesTerminal.iso F))) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (pullback (c.inj i) (c.inj j))))) → (fun (X : Type w) ↦ X) (⊤_ Type w))
        ((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)))) :
      (fun (X : Type w) ↦ X) (⊤_ Type w))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
              (F.mapIso (Iso.op (IsPullback.isoPullback ⋯)) ≪≫
                Iso.trans (Y := F.obj (terminal.{v, u} Cᵒᵖ))
                  (F.mapIso (Iso.symm (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial))))
                  (PreservesTerminal.iso F))) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (pullback (c.inj i) (c.inj j))))) → (fun (X : Type w) ↦ X) (⊤_ Type w))
        ((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)))) :
      (fun (X : Type w) ↦ X) (⊤_ Type w))

Tactic:
ext ⟨i⟩