-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f →
          Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
                x :
              (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
                x :
              (fun (X : Type u_1) ↦ X) (F.obj (op Z)))) ↔
      Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
            x :
          (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
rw :
  (∀ (x : F.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) :
                    (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
                  x :
                (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) :
                    (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op Z)))
                  x :
                (fun (X : Type u_1) ↦ X) (F.obj (op Z)))) →
        ∃! y : (fun (X : Type u_1) ↦ X) (F.obj (op Y)),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op Y))) → (fun (X : Type u_1) ↦ X) (F.obj (op X)))
              y =
            x) ↔
    ∀ (y : F.obj (op X)),
      Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
              y :
            (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op X))) → (fun (X : Type u_1) ↦ X) (F.obj (op c.pt)))
              y :
            (fun (X : Type u_1) ↦ X) (F.obj (op c.pt))) →
        ∃! x : F.obj (op Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_1) ↦ X) (F.obj (op Y))) → (fun (X : Type u_1) ↦ X) (F.obj (op X)))
              x =
            y
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique, Presieve.isSheafFor_singleton]

Premises used: CategoryTheory.Presieve.isSheafFor_singleton, CategoryTheory.Limits.Types.type_equalizer_iff_unique