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

Tactic:
apply h