-- 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
x : FirstObj P S.arrows
t :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P S) :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
        x :
      (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P S) :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) → (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
        x :
      (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
mpr :
  ∀
    (t :
      ∀ (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))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P S) :
                  (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
                    (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
                x) :
            (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))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P S) :
                  (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
                    (fun (X : Type (max u v)) ↦ X) (SecondObj P S))
                x) :
            (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)))
    ⦃Y Z : C⦄ (f : Y ⟶ X) (g : Z ⟶ Y) (hf : S.arrows f),
    Eq (α := P.obj (op Z))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
              (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
          x (g ≫ f) ⋯ :
        P.obj (op Z))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
            (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Y))) → (fun (X : Type (max u v)) ↦ X) (P.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
              (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
                (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
            x f hf) :
        (fun (X : Type (max u v)) ↦ X) (P.obj (op Z)))
⊢ Eq (α := P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
          (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
            (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
        x (g ≫ f) ⋯ :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (P.obj (op Y))) → (fun (X : Type (max u v)) ↦ X) (P.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstObjEqFamily P S.arrows).hom :
            (a : (fun (X : Type (max u v)) ↦ X) (FirstObj P S.arrows)) →
              (fun (X : Type (max u v)) ↦ X) (Presieve.FamilyOfElements P S.arrows))
          x f hf) :
      (fun (X : Type (max u v)) ↦ X) (P.obj (op Z)))

Tactic:
rw [Types.limit_ext_iff'] at t

Premises used: CategoryTheory.Limits.Types.limit_ext_iff'