-- 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 :
  Presieve.FamilyOfElements.PullbackCompatible (P := P) (R := R)
    ((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)
Y : C
f : Y ⟶ X
hf : R f
Z : C
g : Z ⟶ X
hg : R g
⊢ Eq (α :=
    (fun (X : Type (max u v)) ↦ X)
      (Functor.obj (C := Discrete (((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }))
        (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))))
        {
          as :=
            (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf),
              Sigma.mk (β := fun (Z : C) ↦ { g : Z ⟶ X // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ X) ↦ R g) g hg)) }))
    ((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))))
              {
                as :=
                  (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf),
                    Sigma.mk (β := fun (Z : C) ↦ { g : Z ⟶ X // R g }) Z
                      (Subtype.mk (p := fun (g : Z ⟶ X) ↦ R g) g hg)) :
                Discrete (((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) }) :
          (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
                { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }))
        ((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 (C := Discrete (((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }))
          (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))))
          {
            as :=
              (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf),
                Sigma.mk (β := fun (Z : C) ↦ { g : Z ⟶ X // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ X) ↦ R g) g hg)) }))
    ((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))))
              {
                as :=
                  (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf),
                    Sigma.mk (β := fun (Z : C) ↦ { g : Z ⟶ X // R g }) Z
                      (Subtype.mk (p := fun (g : Z ⟶ X) ↦ R g) g hg)) :
                Discrete (((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) }) :
          (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
                { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }))
        ((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 (C := Discrete (((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }))
          (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))))
          {
            as :=
              (Sigma.mk (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ X) ↦ R f) f hf),
                Sigma.mk (β := fun (Z : C) ↦ { g : Z ⟶ X // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ X) ↦ R g) g hg)) }))

Tactic:
simpa [firstMap, secondMap] using t hf hg

Premises used: CategoryTheory.Equalizer.Presieve.firstMap, CategoryTheory.Equalizer.Presieve.secondMap