-- 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
h :
  ∀ (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) (x : P.obj (op X)),
    Eq (α :=
      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))))
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              ∏ᶜ 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))))
              (forkMap P R ≫ firstMap P R :
                P.obj (op X) ⟶
                  ∏ᶜ 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))))
              (Pi.π
                  (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))))
                  fg :
                (∏ᶜ 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)))) ⟶
                  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))))))
          x :
        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))))
      (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              ∏ᶜ 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))))
              (forkMap P R ≫ secondMap P R :
                P.obj (op X) ⟶
                  ∏ᶜ 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))))
              (Pi.π
                  (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))))
                  fg :
                (∏ᶜ 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)))) ⟶
                  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))))))
          x :
        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))))
⊢ Eq (α :=
    P.obj (op X) ⟶
      ∏ᶜ 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))))
    (forkMap P R ≫ firstMap P R :
      P.obj (op X) ⟶
        ∏ᶜ 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))))
    (forkMap P R ≫ secondMap P R :
      P.obj (op X) ⟶
        ∏ᶜ 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))))

Tactic:
ext fg