-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
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
⊢ Eq (α := P.obj (op U) ⟶ secondObj R P) (forkMap R P ≫ firstMap R P) (forkMap R P ≫ secondMap R P)
have 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)
Tactic: apply limit.hom_ext