-- 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)))))))))
w :
  ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' : Y ⟶ X // S.arrows f' })),
    Eq (α :=
      (fun (X : Type (max u v)) ↦ X)
        (Functor.obj
          (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' }))))
          j))
      ((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' }))))
                j) :
            (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
                  j))
          z₁ :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (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' }))))
            j))
      ((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' }))))
                j) :
            (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
                  j))
          z₂ :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (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' }))))
            j))
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Premises used: CategoryTheory.Limits.Types.limit_ext