-- 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
fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }
x : P.obj (op X)
h :
  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 _ types 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))))
            (CategoryStruct.comp (Y := FirstObj P R)
              (Pi.lift (f := fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })))) fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                P.map (↑(f.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : f.fst ⟶ X).op)
              (Pi.lift (f := 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))))
                fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                Pi.π
                    (fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                      P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                    fg.1 ≫
                  P.map
                    (Quiver.Hom.op
                      (pullback.fst (↑(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)))
        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 _ types 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))))
            (CategoryStruct.comp (Y := FirstObj P R)
              (Pi.lift (f := fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })))) fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                P.map (↑(f.snd (β := fun (Y : C) ↦ { f : Y ⟶ X // R f })) : f.fst ⟶ X).op)
              (Pi.lift (f := 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))))
                fun (fg : ((Y : C) × { f : Y ⟶ X // R f }) × (Z : C) × { g : Z ⟶ X // R g }) ↦
                Pi.π
                    (fun (f : (Y : C) × { f : Y ⟶ X // R f }) ↦
                      P.obj (op (f.fst (β := fun (Y : C) ↦ { f : Y ⟶ X // R f }))))
                    fg.2 ≫
                  P.map
                    (Quiver.Hom.op
                      (pullback.snd (↑(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)))
        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
        (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))))

Tactic:
simp only [firstMap, secondMap, forkMap]

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