-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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)))
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))
have 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
Tactic: rw [Types.type_equalizer_iff_unique, Presieve.isSheafFor_singleton]