-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
U : C
R : Presieve.{v₁, u₁} U
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
inst_2 : HasProducts A
inst_3 : HasPullbacks.{v₁, u₁} C
w₁ :
  ∀ (j : Discrete (((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g })),
    Eq (α :=
      P.obj (op U) ⟶
        Functor.obj
          (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
            P.obj
              (op
                (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                  (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
          j)
      (CategoryStruct.comp (Y :=
          limit (J := Discrete (((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }))
            (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
              P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U)))))
          (forkMap R P ≫ firstMap R P : P.obj (op U) ⟶ secondObj R P)
          (limit.π
            (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
              P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
            j) :
        P.obj (op U) ⟶
          Functor.obj
            (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
              P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
            j)
      (CategoryStruct.comp (Y :=
          limit (J := Discrete (((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }))
            (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
              P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U)))))
          (forkMap R P ≫ secondMap R P : P.obj (op U) ⟶ secondObj R P)
          (limit.π
            (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
              P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
            j) :
        P.obj (op U) ⟶
          Functor.obj
            (Discrete.functor fun (fg : ((V : C) × { f : V ⟶ U // R f }) × (W : C) × { g : W ⟶ U // R g }) ↦
              P.obj
                (op
                  (Limits.pullback (↑(fg.1.snd (β := fun (V : C) ↦ { f : V ⟶ U // R f })) : fg.1.fst ⟶ U)
                    (↑(fg.2.snd (β := fun (W : C) ↦ { g : W ⟶ U // R g })) : fg.2.fst ⟶ U))))
            j)
⊢ Eq (α := P.obj (op U) ⟶ secondObj R P) (forkMap R P ≫ firstMap R P) (forkMap R P ≫ secondMap R P)

Tactic:
apply limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext