-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
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))))))
⊢ z₁ = z₂
have w : ∀ (j : Discrete ((Y : C) × { f : Y ⟶ X // R f })),
  Eq (α :=
    (fun (X : Type (max u v)) ↦ X)
      (Functor.obj
        (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
          P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
        j))
    ((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 }))))
              j) :
          (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 j))
        z₁ :
      (fun (X : Type (max u v)) ↦ X)
        (Functor.obj
          (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
            P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
          j))
    ((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 }))))
              j) :
          (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 j))
        z₂ :
      (fun (X : Type (max u v)) ↦ X)
        (Functor.obj
          (Discrete.functor fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
            P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
          j))
Tactic: apply Limits.Types.limit_ext