case w
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ ∀ (j : Discrete (((V : C) × { f // R f }) × (W : C) × { g // R g })),
    (forkMap R P ≫ firstMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j =
      (forkMap R P ≫ secondMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P
apply limit.hom_ext
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ (forkMap R P ≫ firstMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        {
          as :=
            ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) } =
    (forkMap R P ≫ secondMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
case w
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
⊢ ∀ (j : Discrete (((V : C) × { f // R f }) × (W : C) × { g // R g })),
    (forkMap R P ≫ firstMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j =
      (forkMap R P ≫ secondMap R P) ≫
        limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op) j
rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map f.op ≫ P.map pullback.fst.op = P.map g.op ≫ P.map pullback.snd.op
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ (forkMap R P ≫ firstMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        {
          as :=
            ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) } =
    (forkMap R P ≫ secondMap R P) ≫
      limit.π (Discrete.functor fun fg => P.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        { as := ({ fst := Y, snd := { val := f, property := hf } }, { fst := Z, snd := { val := g, property := hg } }) }
simp only [firstMap, secondMap, forkMap, limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app,
  Subtype.coe_mk]
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (pullback.snd ≫ g).op = P.map g.op ≫ P.map pullback.snd.op
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map f.op ≫ P.map pullback.fst.op = P.map g.op ≫ P.map pullback.snd.op
rw [← P.map_comp, ← op_comp, pullback.condition]
no goals
case w.mk.mk.mk.mk.mk.mk
C : Type u₁
inst✝³ : Category C
A : Type u₂
inst✝² : Category A
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (pullback.snd ≫ g).op = P.map g.op ≫ P.map pullback.snd.op
simp