-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
Goal:
C : Type u
inst : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve.{v, u} X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    Eq (α :=
      (fun (X : Type (max u v)) ↦ X)
        (P.obj
          (op
            (Sigma.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })
              (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π
                (fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                  P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))) :
            (a : (fun (X : Type (max u v)) ↦ X) (∏ᶜ fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst))) →
              (fun (X : Type (max u v)) ↦ X) (P.obj (op ⟨Y, ⟨f, hf⟩⟩.fst)))
          z₁ :
        (fun (X : Type (max u v)) ↦ X)
          (P.obj
            (op
              (Sigma.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y
                  (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Pi.π
                (fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                  P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))) :
            (a : (fun (X : Type (max u v)) ↦ X) (∏ᶜ fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst))) →
              (fun (X : Type (max u v)) ↦ X) (P.obj (op ⟨Y, ⟨f, hf⟩⟩.fst)))
          z₂ :
        (fun (X : Type (max u v)) ↦ X)
          (P.obj
            (op
              (Sigma.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })
                (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y
                  (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf))))))
Y : C
f : Y ⟶ X
hf : R f
⊢ Eq (α :=
    (fun (X : Type (max u v)) ↦ X)
      (Functor.obj (C := Discrete ((Y : C) × { f : Y ⟶ X // R f }))
        (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
          P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
        { as := Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf) }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (limit.π
              (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
              {
                as :=
                  Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf) :
                Discrete ((Y : C) × { f : Y ⟶ X // R f }) }) :
          (a :
              (fun (X : Type (max u v)) ↦ X)
                (limit (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)))) →
            (fun (X : Type (max u v)) ↦ X)
              ((Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)).obj
                { as := ⟨Y, ⟨f, hf⟩⟩ }))
        z₁ :
      (fun (X : Type (max u v)) ↦ X)
        (Functor.obj (C := Discrete ((Y : C) × { f : Y ⟶ X // R f }))
          (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
            P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
          {
            as :=
              Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf) }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (limit.π
              (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
              {
                as :=
                  Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf) :
                Discrete ((Y : C) × { f : Y ⟶ X // R f }) }) :
          (a :
              (fun (X : Type (max u v)) ↦ X)
                (limit (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)))) →
            (fun (X : Type (max u v)) ↦ X)
              ((Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦ P.obj (op f.fst)).obj
                { as := ⟨Y, ⟨f, hf⟩⟩ }))
        z₂ :
      (fun (X : Type (max u v)) ↦ X)
        (Functor.obj (C := Discrete ((Y : C) × { f : Y ⟶ X // R f }))
          (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
            P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
          {
            as :=
              Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf) }))

Tactic:
h Y f hf