-- 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
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
w₁ :
  Eq (α :=
    P.obj (op U) ⟶
      Functor.obj (C := 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))))
        {
          as :=
            (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
              Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) })
    (P.map f.op ≫ P.map (Quiver.Hom.op (pullback.fst f g))) (P.map g.op ≫ P.map (Quiver.Hom.op (pullback.snd f g)))
⊢ Eq (α :=
    P.obj (op U) ⟶
      Functor.obj (C := 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))))
        {
          as :=
            (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
              Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) })
    (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))))
          {
            as :=
              (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
                Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z
                  (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) }) :
      P.obj (op U) ⟶
        Functor.obj (C := 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))))
          {
            as :=
              (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
                Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) })
    (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))))
          {
            as :=
              (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
                Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z
                  (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) }) :
      P.obj (op U) ⟶
        Functor.obj (C := 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))))
          {
            as :=
              (Sigma.mk (β := fun (V : C) ↦ { f : V ⟶ U // R f }) Y (Subtype.mk (p := fun (f : Y ⟶ U) ↦ R f) f hf),
                Sigma.mk (β := fun (W : C) ↦ { g : W ⟶ U // R g }) Z (Subtype.mk (p := fun (g : Z ⟶ U) ↦ R g) g hg)) })

Tactic:
simp only [firstMap, secondMap, forkMap, limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app,
    Subtype.coe_mk]

Premises used: Subtype.coe_mk, CategoryTheory.Category.assoc, CategoryTheory.Presheaf.forkMap, CategoryTheory.Presheaf.secondMap, CategoryTheory.Presheaf.firstMap, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app