-- 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
inst_1 : R.HasPairwisePullbacks
x : FirstObj P R
t :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
        x :
      (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
        x :
      (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
hf : R f
hg : R g
mpr :
  ∀
    (t :
      ∀ (j : Discrete (((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g })),
        Eq (α :=
          (fun (X : Type (max u v)) ↦ X)
            (Functor.obj
              (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                P.obj
                  (op
                    (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
                      (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X))))
              j))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (limit.π
                    (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                      P.obj
                        (op
                          (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
                            (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X))))
                    j) :
                (a :
                    (fun (X : Type (max u v)) ↦ X)
                      (limit
                        (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                          P.obj (op (Limits.pullback (↑fg.1.snd : fg.1.fst ⟶ X) (↑fg.2.snd : fg.2.fst ⟶ X)))))) →
                  (fun (X : Type (max u v)) ↦ X)
                    ((Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                          P.obj (op (Limits.pullback (↑fg.1.snd : fg.1.fst ⟶ X) (↑fg.2.snd : fg.2.fst ⟶ X)))).obj
                      j))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P R) :
                  (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
                x) :
            (fun (X : Type (max u v)) ↦ X)
              (Functor.obj
                (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                  P.obj
                    (op
                      (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
                        (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X))))
                j))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (limit.π
                    (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                      P.obj
                        (op
                          (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
                            (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X))))
                    j) :
                (a :
                    (fun (X : Type (max u v)) ↦ X)
                      (limit
                        (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                          P.obj (op (Limits.pullback (↑fg.1.snd : fg.1.fst ⟶ X) (↑fg.2.snd : fg.2.fst ⟶ X)))))) →
                  (fun (X : Type (max u v)) ↦ X)
                    ((Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                          P.obj (op (Limits.pullback (↑fg.1.snd : fg.1.fst ⟶ X) (↑fg.2.snd : fg.2.fst ⟶ X)))).obj
                      j))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P R) :
                  (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P R))
                x) :
            (fun (X : Type (max u v)) ↦ X)
              (Functor.obj
                (Discrete.functor fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                  P.obj
                    (op
                      (Limits.pullback (↑(fg.1.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : fg.1.fst ⟶ X)
                        (↑(fg.2.snd (β := fun (Z : C) ↦ { g : Z ⟶ X // R g })) : fg.2.fst ⟶ X))))
                j)))
    ⦃Y Z : C⦄ ⦃f : Y ⟶ X⦄ ⦃g : Z ⟶ X⦄ (hf : R f) (hg : R g),
    Eq (α := (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst f g))) :
            (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Y))) →
              (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
              (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
                (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
            x f hf) :
        (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd f g))) :
            (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Z))) →
              (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
              (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
                (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
            x g hg) :
        (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst f g))) :
          (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Y))) →
            (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
              (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
          x f hf) :
      (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd f g))) :
          (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Z))) →
            (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P R).hom :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P R)) →
              (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P R))
          x g hg) :
      (fun (X : Type (max u v)) ↦ X) (P.obj (op (Limits.pullback f g))))

Tactic:
rw [Types.limit_ext_iff'] at t

Premises used: CategoryTheory.Limits.Types.limit_ext_iff'