-- 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)))
simp_rw simp_rw₁ :
  (∀ (x : F.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f →
            Eq (α := F.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₁.op) : (a : F.obj (op X)) → F.obj (op Z)) x :
                F.obj (op Z))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map p₂.op) : (a : F.obj (op X)) → F.obj (op Z)) x :
                F.obj (op Z))) →
        ∃! y : F.obj (op Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) : (a : F.obj (op Y)) → F.obj (op X)) y = x) ↔
    ∀ (y : F.obj (op X)),
      Eq (α := F.obj (op c.pt))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.fst.op) : (a : F.obj (op X)) → F.obj (op c.pt)) y :
            F.obj (op c.pt))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map c.snd.op) : (a : F.obj (op X)) → F.obj (op c.pt)) y :
            F.obj (op c.pt)) →
        ∃! x : F.obj (op Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) : (a : F.obj (op Y)) → F.obj (op X)) x = y
⊢ (∀ (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:
simp_rw [h]