case w
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (forkMap P S.arrows ≫ firstMap P S) ≫ limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j =
      (forkMap P S.arrows ≫ secondMap P S) ≫ limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ forkMap P S.arrows ≫ firstMap P S = forkMap P S.arrows ≫ secondMap P S
apply limit.hom_ext
case w.mk.mk.mk.mk.mk
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ (forkMap P S.arrows ≫ firstMap P S) ≫
      limit.π (Discrete.functor fun f => P.obj f.snd.fst.op)
        { as := { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } } =
    (forkMap P S.arrows ≫ secondMap P S) ≫
      limit.π (Discrete.functor fun f => P.obj f.snd.fst.op)
        { as := { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } }
case w
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
⊢ ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    (forkMap P S.arrows ≫ firstMap P S) ≫ limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j =
      (forkMap P S.arrows ≫ secondMap P S) ≫ limit.π (Discrete.functor fun f => P.obj f.snd.fst.op) j
rintro ⟨Y, Z, g, f, hf⟩
no goals
case w.mk.mk.mk.mk.mk
C : Type u₁
inst✝ : Category C
P : Cᵒᵖ ⥤ Type (max v₁ u₁)
X : C
R : Presieve X
S : Sieve X
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ (forkMap P S.arrows ≫ firstMap P S) ≫
      limit.π (Discrete.functor fun f => P.obj f.snd.fst.op)
        { as := { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } } =
    (forkMap P S.arrows ≫ secondMap P S) ≫
      limit.π (Discrete.functor fun f => P.obj f.snd.fst.op)
        { as := { fst := Y, snd := { fst := Z, snd := { fst := g, snd := { val := f, property := hf } } } } }
simp [firstMap, secondMap, forkMap]