[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
i : ι
⊢ res F U ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := i } = F.map (leSupr U i).op
[PROOFSTEP]
rw [res, limit.lift_π, Fan.mk_π_app]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
⊢ res F U ≫ leftRes F U = res F U ≫ rightRes F U
[PROOFSTEP]
dsimp [res, leftRes, rightRes]
  -- Porting note : `ext` can't see `limit.hom_ext` applies here:
    -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
⊢ ((Pi.lift fun i => F.map (leSupr U i).op) ≫
      Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) =
    (Pi.lift fun i => F.map (leSupr U i).op) ≫
      Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
[PROOFSTEP]
refine limit.hom_ext (fun _ => ?_)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) x✝ =
    ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) x✝
[PROOFSTEP]
simp only [limit.lift_π, limit.lift_π_assoc, Fan.mk_π_app, Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map (leSupr U x✝.as.fst).op ≫ F.map (infLELeft (U x✝.as.fst) (U x✝.as.snd)).op =
    F.map (leSupr U x✝.as.snd).op ≫ F.map (infLERight (U x✝.as.fst) (U x✝.as.snd)).op
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U x✝.as.fst).op ≫ (infLELeft (U x✝.as.fst) (U x✝.as.snd)).op) =
    F.map (leSupr U x✝.as.snd).op ≫ F.map (infLERight (U x✝.as.fst) (U x✝.as.snd)).op
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
x✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U x✝.as.fst).op ≫ (infLELeft (U x✝.as.fst) (U x✝.as.snd)).op) =
    F.map ((leSupr U x✝.as.snd).op ≫ (infLERight (U x✝.as.fst) (U x✝.as.snd)).op)
[PROOFSTEP]
congr 1
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (X_1 : WalkingParallelPair) → (diagram F U).obj X_1 ≅ (diagram G U).obj X_1
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).obj WalkingParallelPair.zero ≅ (diagram G U).obj WalkingParallelPair.zero
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).obj WalkingParallelPair.one ≅ (diagram G U).obj WalkingParallelPair.one
[PROOFSTEP]
exact piOpens.isoOfIso U α
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).obj WalkingParallelPair.one ≅ (diagram G U).obj WalkingParallelPair.one
[PROOFSTEP]
exact piInters.isoOfIso U α
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ ∀ {X_1 Y : WalkingParallelPair} (f : X_1 ⟶ Y),
    (diagram F U).map f ≫ (WalkingParallelPair.casesOn Y (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
      (WalkingParallelPair.casesOn X_1 (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫ (diagram G U).map f
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map (WalkingParallelPairHom.id WalkingParallelPair.zero)
[PROOFSTEP]
simp
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map WalkingParallelPairHom.left ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map WalkingParallelPairHom.left
[PROOFSTEP]
refine limit.hom_ext (fun _ => ?_)
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
x✝ : Discrete (ι × ι)
⊢ ((diagram F U).map WalkingParallelPairHom.left ≫
        (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom) ≫
      limit.π (Discrete.functor fun p => G.obj (op (U p.fst ⊓ U p.snd))) x✝ =
    ((WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
        (diagram G U).map WalkingParallelPairHom.left) ≫
      limit.π (Discrete.functor fun p => G.obj (op (U p.fst ⊓ U p.snd))) x✝
[PROOFSTEP]
simp only [leftRes, piOpens.isoOfIso, piInters.isoOfIso, parallelPair_map_left, Functor.mapIso_hom, lim_map,
  limit.lift_map, limit.lift_π, Cones.postcompose_obj_π, NatTrans.comp_app, Fan.mk_π_app, Discrete.natIso_hom_app,
  Iso.app_hom, Category.assoc, NatTrans.naturality, limMap_π_assoc]
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map WalkingParallelPairHom.right ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map WalkingParallelPairHom.right
[PROOFSTEP]
refine limit.hom_ext (fun _ => ?_)
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
x✝ : Discrete (ι × ι)
⊢ ((diagram F U).map WalkingParallelPairHom.right ≫
        (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom) ≫
      limit.π (Discrete.functor fun p => G.obj (op (U p.fst ⊓ U p.snd))) x✝ =
    ((WalkingParallelPair.casesOn WalkingParallelPair.zero (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
        (diagram G U).map WalkingParallelPairHom.right) ≫
      limit.π (Discrete.functor fun p => G.obj (op (U p.fst ⊓ U p.snd))) x✝
[PROOFSTEP]
simp only [rightRes, piOpens.isoOfIso, piInters.isoOfIso, parallelPair_map_right, Functor.mapIso_hom, lim_map,
  limit.lift_map, limit.lift_π, Cones.postcompose_obj_π, NatTrans.comp_app, Fan.mk_π_app, Discrete.natIso_hom_app,
  Iso.app_hom, Category.assoc, NatTrans.naturality, limMap_π_assoc]
[GOAL]
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.one (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫
      (diagram G U).map (WalkingParallelPairHom.id WalkingParallelPair.one)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ fork F U ≅ (Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)
[PROOFSTEP]
fapply Fork.ext
[GOAL]
case i
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ (fork F U).pt ≅ ((Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)).pt
[PROOFSTEP]
apply α.app
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ autoParam
    ((α.app (op (iSup U))).hom ≫ Fork.ι ((Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)) =
      Fork.ι (fork F U))
    _auto✝
[PROOFSTEP]
refine limit.hom_ext (fun _ => ?_)
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
x✝ : Discrete ι
⊢ ((α.app (op (iSup U))).hom ≫ Fork.ι ((Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U))) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) x✝ =
    Fork.ι (fork F U) ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) x✝
[PROOFSTEP]
dsimp only [Fork.ι]
  -- Ugh, `simp` can't unfold abbreviations.
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
x✝ : Discrete ι
⊢ ((α.app (op (iSup U))).hom ≫
        NatTrans.app ((Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)).π WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) x✝ =
    NatTrans.app (fork F U).π WalkingParallelPair.zero ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) x✝
[PROOFSTEP]
simp only [res, diagram.isoOfIso, Iso.app_hom, piOpens.isoOfIso, Cones.postcompose_obj_π, NatTrans.comp_app,
  fork_π_app_walkingParallelPair_zero, NatIso.ofComponents_inv_app, Functor.mapIso_inv, lim_map, limit.lift_map,
  Category.assoc, limit.lift_π, Fan.mk_π_app, Discrete.natIso_inv_app, Iso.app_inv, NatTrans.naturality,
  Iso.hom_inv_id_app_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Y Z : WalkingParallelPair
f : Y ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        Z =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        Y ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
[PROOFSTEP]
cases Y
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Z : WalkingParallelPair
f : WalkingParallelPair.zero ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        Z =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
[PROOFSTEP]
cases Z
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
Z : WalkingParallelPair
f : WalkingParallelPair.one ⟶ Z
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        Z =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
[PROOFSTEP]
cases Z
[GOAL]
case zero.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.zero
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
[PROOFSTEP]
cases f
[GOAL]
case zero.one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.zero ⟶ WalkingParallelPair.one
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
[PROOFSTEP]
cases f
[GOAL]
case one.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.zero
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
[PROOFSTEP]
cases f
[GOAL]
case one.one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
f : WalkingParallelPair.one ⟶ WalkingParallelPair.one
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map f ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one ≫
      (SheafConditionEqualizerProducts.diagram F U).map f
[PROOFSTEP]
cases f
[GOAL]
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.zero)
[PROOFSTEP]
refine limit.hom_ext fun i => ?_
[GOAL]
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete ι
⊢ (((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
        (fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) i =
    ((fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.zero ≫
        (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.zero)) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) i
[PROOFSTEP]
dsimp
[GOAL]
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete ι
⊢ (𝟙 c.pt ≫ Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) i =
    ((Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.zero)) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) i
[PROOFSTEP]
simp only [limit.lift_π, Category.id_comp, Fan.mk_π_app, CategoryTheory.Functor.map_id, Category.assoc]
[GOAL]
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete ι
⊢ NatTrans.app c.π (op (single i.as)) =
    (Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫
      𝟙 ((SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.zero) ≫
        limit.π (Discrete.functor fun i => F.obj (op (U i))) i
[PROOFSTEP]
dsimp
[GOAL]
case zero.zero.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete ι
⊢ NatTrans.app c.π (op (single i.as)) =
    (Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫
      𝟙 (SheafConditionEqualizerProducts.piOpens F U) ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) i
[PROOFSTEP]
simp only [limit.lift_π, Category.id_comp, Fan.mk_π_app]
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.left ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left
[PROOFSTEP]
refine limit.hom_ext fun ⟨i, j⟩ => ?_
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.left ≫
        (fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    ((fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.zero ≫
        (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
dsimp [SheafConditionEqualizerProducts.leftRes]
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 c.pt ≫ Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    ((Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
⊢ NatTrans.app c.π (op (Pairwise.pair i j)) = NatTrans.app c.π (op (single i)) ≫ F.map (infLELeft (U i) (U j)).op
[PROOFSTEP]
have h := c.π.naturality (Quiver.Hom.op (Hom.left i j))
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
h :
  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (left i j).op ≫
      NatTrans.app c.π (op (Pairwise.pair i j)) =
    NatTrans.app c.π (op (single i)) ≫ ((diagram U).op ⋙ F).map (left i j).op
⊢ NatTrans.app c.π (op (Pairwise.pair i j)) = NatTrans.app c.π (op (single i)) ≫ F.map (infLELeft (U i) (U j)).op
[PROOFSTEP]
dsimp at h 
[GOAL]
case zero.one.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
h :
  𝟙 c.pt ≫ NatTrans.app c.π (op (Pairwise.pair i j)) =
    NatTrans.app c.π (op (single i)) ≫ F.map ((diagram U).map (left i j)).op
⊢ NatTrans.app c.π (op (Pairwise.pair i j)) = NatTrans.app c.π (op (single i)) ≫ F.map (infLELeft (U i) (U j)).op
[PROOFSTEP]
simpa using h
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.right ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.right
[PROOFSTEP]
refine limit.hom_ext fun ⟨i, j⟩ => ?_
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.right ≫
        (fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    ((fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.zero ≫
        (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.right) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
dsimp [SheafConditionEqualizerProducts.rightRes]
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 c.pt ≫ Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    ((Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
⊢ NatTrans.app c.π (op (Pairwise.pair i j)) = NatTrans.app c.π (op (single j)) ≫ F.map (infLERight (U i) (U j)).op
[PROOFSTEP]
have h := c.π.naturality (Quiver.Hom.op (Hom.right i j))
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
h :
  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (right i j).op ≫
      NatTrans.app c.π (op (Pairwise.pair i j)) =
    NatTrans.app c.π (op (single j)) ≫ ((diagram U).op ⋙ F).map (right i j).op
⊢ NatTrans.app c.π (op (Pairwise.pair i j)) = NatTrans.app c.π (op (single j)) ≫ F.map (infLERight (U i) (U j)).op
[PROOFSTEP]
dsimp at h 
[GOAL]
case zero.one.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
x✝ : Discrete (ι × ι)
i j : ι
h :
  𝟙 c.pt ≫ NatTrans.app c.π (op (Pairwise.pair i j)) =
    NatTrans.app c.π (op (single j)) ≫ F.map ((diagram U).map (right i j)).op
⊢ NatTrans.app c.π (op (Pairwise.pair i j)) = NatTrans.app c.π (op (single j)) ≫ F.map (infLERight (U i) (U j)).op
[PROOFSTEP]
simpa using h
[GOAL]
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one =
    (fun Z =>
          WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
            (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
        WalkingParallelPair.one ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one)
[PROOFSTEP]
refine limit.hom_ext fun i => ?_
[GOAL]
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete (ι × ι)
⊢ (((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
        (fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i =
    ((fun Z =>
            WalkingParallelPair.casesOn Z (Pi.lift fun i => NatTrans.app c.π (op (single i)))
              (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))))
          WalkingParallelPair.one ≫
        (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one)) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i
[PROOFSTEP]
dsimp
[GOAL]
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete (ι × ι)
⊢ (𝟙 c.pt ≫ Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i =
    ((Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
        (SheafConditionEqualizerProducts.diagram F U).map (𝟙 WalkingParallelPair.one)) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i
[PROOFSTEP]
simp only [limit.lift_π, Category.id_comp, Fan.mk_π_app, CategoryTheory.Functor.map_id, Category.assoc]
[GOAL]
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete (ι × ι)
⊢ NatTrans.app c.π (op (Pairwise.pair i.as.fst i.as.snd)) =
    (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
      𝟙 ((SheafConditionEqualizerProducts.diagram F U).obj WalkingParallelPair.one) ≫
        limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i
[PROOFSTEP]
dsimp
[GOAL]
case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
i : Discrete (ι × ι)
⊢ NatTrans.app c.π (op (Pairwise.pair i.as.fst i.as.snd)) =
    (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
      𝟙 (SheafConditionEqualizerProducts.piInters F U) ≫
        limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i
[PROOFSTEP]
simp only [limit.lift_π, Category.id_comp, Fan.mk_π_app]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
j : WalkingParallelPair
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivFunctorObj F U c) c').π j =
    NatTrans.app ((fun c => coneEquivFunctorObj F U c) c).π j
[PROOFSTEP]
cases j
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivFunctorObj F U c) c').π WalkingParallelPair.zero =
    NatTrans.app ((fun c => coneEquivFunctorObj F U c) c).π WalkingParallelPair.zero
[PROOFSTEP]
refine limit.hom_ext fun i => ?_
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
i : Discrete ι
⊢ (f.Hom ≫ NatTrans.app ((fun c => coneEquivFunctorObj F U c) c').π WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) i =
    NatTrans.app ((fun c => coneEquivFunctorObj F U c) c).π WalkingParallelPair.zero ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) i
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Limits.ConeMorphism.w, Limits.limit.lift_π, Category.assoc, coneEquivFunctorObj_π_app]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivFunctorObj F U c) c').π WalkingParallelPair.one =
    NatTrans.app ((fun c => coneEquivFunctorObj F U c) c).π WalkingParallelPair.one
[PROOFSTEP]
refine limit.hom_ext fun i => ?_
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone ((diagram U).op ⋙ F)
f : c ⟶ c'
i : Discrete (ι × ι)
⊢ (f.Hom ≫ NatTrans.app ((fun c => coneEquivFunctorObj F U c) c').π WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i =
    NatTrans.app ((fun c => coneEquivFunctorObj F U c) c).π WalkingParallelPair.one ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) i
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Limits.ConeMorphism.w, Limits.limit.lift_π, Category.assoc, coneEquivFunctorObj_π_app]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ (X_1 : (CategoryTheory.Pairwise ι)ᵒᵖ) →
    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).obj X_1 ⟶ ((diagram U).op ⋙ F).obj X_1
[PROOFSTEP]
intro x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).obj x ⟶ ((diagram U).op ⋙ F).obj x
[PROOFSTEP]
induction x using Opposite.rec' with
| h x => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).obj x ⟶ ((diagram U).op ⋙ F).obj x
[PROOFSTEP]
induction x using Opposite.rec' with
| h x => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x : CategoryTheory.Pairwise ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).obj (op x) ⟶ ((diagram U).op ⋙ F).obj (op x)
[PROOFSTEP]
rcases x with (⟨i⟩ | ⟨i, j⟩)
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).obj (op (single i)) ⟶
    ((diagram U).op ⋙ F).obj (op (single i))
[PROOFSTEP]
exact c.π.app WalkingParallelPair.zero ≫ Pi.π _ i
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).obj (op (Pairwise.pair i j)) ⟶
    ((diagram U).op ⋙ F).obj (op (Pairwise.pair i j))
[PROOFSTEP]
exact c.π.app WalkingParallelPair.one ≫ Pi.π _ (i, j)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ ∀ ⦃X_1 Y : (CategoryTheory.Pairwise ι)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
        Opposite.rec'
          (fun x =>
            Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
              fun i j =>
              NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
          Y =
      Opposite.rec'
          (fun x =>
            Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
              fun i j =>
              NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
          X_1 ≫
        ((diagram U).op ⋙ F).map f
[PROOFSTEP]
intro x y f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : (CategoryTheory.Pairwise ι)ᵒᵖ
f : x ⟶ y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        y =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        x ≫
      ((diagram U).op ⋙ F).map f
[PROOFSTEP]
induction x using Opposite.rec' with
| h x => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : (CategoryTheory.Pairwise ι)ᵒᵖ
f : x ⟶ y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        y =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        x ≫
      ((diagram U).op ⋙ F).map f
[PROOFSTEP]
induction x using Opposite.rec' with
| h x => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
y : (CategoryTheory.Pairwise ι)ᵒᵖ
x : CategoryTheory.Pairwise ι
f : op x ⟶ y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        y =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f
[PROOFSTEP]
induction y using Opposite.rec' with
| h y => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
y : (CategoryTheory.Pairwise ι)ᵒᵖ
x : CategoryTheory.Pairwise ι
f : op x ⟶ y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        y =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f
[PROOFSTEP]
induction y using Opposite.rec' with
| h y => ?_
[GOAL]
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op y) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f
[PROOFSTEP]
have ef : f = f.unop.op := rfl
[GOAL]
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
ef : f = f.unop.op
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op y) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f
[PROOFSTEP]
revert ef
[GOAL]
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ f = f.unop.op →
    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
        Opposite.rec'
          (fun x =>
            Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
              fun i j =>
              NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
          (op y) =
      Opposite.rec'
          (fun x =>
            Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
              fun i j =>
              NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
          (op x) ≫
        ((diagram U).op ⋙ F).map f
[PROOFSTEP]
generalize f.unop = f'
[GOAL]
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
f' : (op y).unop ⟶ (op x).unop
⊢ f = f'.op →
    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
        Opposite.rec'
          (fun x =>
            Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
              fun i j =>
              NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
          (op y) =
      Opposite.rec'
          (fun x =>
            Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
              fun i j =>
              NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
          (op x) ≫
        ((diagram U).op ⋙ F).map f
[PROOFSTEP]
rintro rfl
[GOAL]
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x y : CategoryTheory.Pairwise ι
f' : (op y).unop ⟶ (op x).unop
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op y) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f'.op
[PROOFSTEP]
rcases x with (⟨i⟩ | ⟨⟩)
[GOAL]
case h.h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
y : CategoryTheory.Pairwise ι
i : ι
f' : (op y).unop ⟶ (op (single i)).unop
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op y) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map f'.op
[PROOFSTEP]
rcases y with (⟨⟩ | ⟨j, j⟩)
[GOAL]
case h.h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
y : CategoryTheory.Pairwise ι
a✝¹ a✝ : ι
f' : (op y).unop ⟶ (op (Pairwise.pair a✝¹ a✝)).unop
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op y) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) ≫
      ((diagram U).op ⋙ F).map f'.op
[PROOFSTEP]
rcases y with (⟨⟩ | ⟨j, j⟩)
[GOAL]
case h.h.single.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i a✝ : ι
f' : (op (single a✝)).unop ⟶ (op (single i)).unop
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single a✝)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map f'.op
[PROOFSTEP]
rcases f' with ⟨⟩
[GOAL]
case h.h.single.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j✝ j : ι
f' : (op (Pairwise.pair j✝ j)).unop ⟶ (op (single i)).unop
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair j✝ j)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map f'.op
[PROOFSTEP]
rcases f' with ⟨⟩
[GOAL]
case h.h.pair.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝² a✝¹ a✝ : ι
f' : (op (single a✝)).unop ⟶ (op (Pairwise.pair a✝² a✝¹)).unop
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single a✝)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair a✝² a✝¹)) ≫
      ((diagram U).op ⋙ F).map f'.op
[PROOFSTEP]
rcases f' with ⟨⟩
[GOAL]
case h.h.pair.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ j✝ j : ι
f' : (op (Pairwise.pair j✝ j)).unop ⟶ (op (Pairwise.pair a✝¹ a✝)).unop
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f'.op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair j✝ j)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) ≫
      ((diagram U).op ⋙ F).map f'.op
[PROOFSTEP]
rcases f' with ⟨⟩
[GOAL]
case h.h.single.single.id_single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (id_single i).op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single i)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map (id_single i).op
[PROOFSTEP]
dsimp
[GOAL]
case h.h.single.single.id_single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i) ≫ F.map ((diagram U).map (id_single i)).op
[PROOFSTEP]
erw [F.map_id]
[GOAL]
case h.h.single.single.id_single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i : ι
⊢ 𝟙 c.pt ≫ Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i =
    (Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i) ≫ 𝟙 (F.obj (op ((diagram U).obj (single i))))
[PROOFSTEP]
simp
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (left i j).op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair i j)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map (left i j).op
[PROOFSTEP]
dsimp
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ 𝟙 c.pt ≫ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    (Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i) ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
simp only [Category.id_comp, Category.assoc]
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
have h := c.π.naturality WalkingParallelPairHom.left
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.left ≫
      NatTrans.app c.π WalkingParallelPair.one =
    NatTrans.app c.π WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.left
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
dsimp [SheafConditionEqualizerProducts.leftRes] at h 
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  𝟙 c.pt ≫ NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
simp only [Category.id_comp] at h 
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
have h' := h =≫ Pi.π _ (i, j)
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op
h' :
  NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j)
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
rw [h']
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op
h' :
  NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j)
⊢ (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
simp only [Category.assoc, limit.lift_π, Fan.mk_π_app]
[GOAL]
case h.h.single.pair.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op
h' :
  NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j)
⊢ Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map (infLELeft (U i) (U j)).op =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (left i j)).op
[PROOFSTEP]
rfl
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (right j i).op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair j i)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (single i)) ≫
      ((diagram U).op ⋙ F).map (right j i).op
[PROOFSTEP]
dsimp
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ 𝟙 c.pt ≫ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    (Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i) ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
simp only [Category.id_comp, Category.assoc]
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
have h := c.π.naturality WalkingParallelPairHom.right
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  ((Functor.const WalkingParallelPair).obj c.pt).map WalkingParallelPairHom.right ≫
      NatTrans.app c.π WalkingParallelPair.one =
    NatTrans.app c.π WalkingParallelPair.zero ≫
      (SheafConditionEqualizerProducts.diagram F U).map WalkingParallelPairHom.right
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
dsimp [SheafConditionEqualizerProducts.rightRes] at h 
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  𝟙 c.pt ≫ NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
simp only [Category.id_comp] at h 
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
have h' := h =≫ Pi.π _ (j, i)
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
h' :
  NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i)
⊢ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
rw [h']
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
h' :
  NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i)
⊢ (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
simp
[GOAL]
case h.h.single.pair.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
i j : ι
h :
  NatTrans.app c.π WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
h' :
  NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i) =
    (Fork.ι c ≫ Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (j, i)
⊢ Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map (infLERight (U j) (U i)).op =
    Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i ≫ F.map ((diagram U).map (right j i)).op
[PROOFSTEP]
rfl
[GOAL]
case h.h.pair.pair.id_pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map (id_pair a✝¹ a✝).op ≫
      Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) =
    Opposite.rec'
        (fun x =>
          Pairwise.casesOn x (fun i => NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i)
            fun i j => NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j))
        (op (Pairwise.pair a✝¹ a✝)) ≫
      ((diagram U).op ⋙ F).map (id_pair a✝¹ a✝).op
[PROOFSTEP]
dsimp
[GOAL]
case h.h.pair.pair.id_pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ 𝟙 c.pt ≫ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝) =
    (NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝)) ≫
      F.map ((diagram U).map (id_pair a✝¹ a✝)).op
[PROOFSTEP]
erw [F.map_id]
[GOAL]
case h.h.pair.pair.id_pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
a✝¹ a✝ : ι
⊢ 𝟙 c.pt ≫ NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝) =
    (NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝)) ≫
      𝟙 (F.obj (op ((diagram U).obj (Pairwise.pair a✝¹ a✝))))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    f.Hom ≫ NatTrans.app ((fun c => coneEquivInverseObj F U c) c').π j =
      NatTrans.app ((fun c => coneEquivInverseObj F U c) c).π j
[PROOFSTEP]
intro x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivInverseObj F U c) c').π x =
    NatTrans.app ((fun c => coneEquivInverseObj F U c) c).π x
[PROOFSTEP]
induction x using Opposite.rec' with
| h x => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivInverseObj F U c) c').π x =
    NatTrans.app ((fun c => coneEquivInverseObj F U c) c).π x
[PROOFSTEP]
induction x using Opposite.rec' with
| h x => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
x : CategoryTheory.Pairwise ι
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivInverseObj F U c) c').π (op x) =
    NatTrans.app ((fun c => coneEquivInverseObj F U c) c).π (op x)
[PROOFSTEP]
rcases x with (⟨i⟩ | ⟨i, j⟩)
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivInverseObj F U c) c').π (op (single i)) =
    NatTrans.app ((fun c => coneEquivInverseObj F U c) c).π (op (single i))
[PROOFSTEP]
dsimp
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ f.Hom ≫ Fork.ι c' ≫ Pi.π (fun i => F.obj (op (U i))) i = Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i
[PROOFSTEP]
dsimp only [Fork.ι]
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i : ι
⊢ f.Hom ≫ NatTrans.app c'.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i =
    NatTrans.app c.π WalkingParallelPair.zero ≫ Pi.π (fun i => F.obj (op (U i))) i
[PROOFSTEP]
rw [← f.w WalkingParallelPair.zero, Category.assoc]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ f.Hom ≫ NatTrans.app ((fun c => coneEquivInverseObj F U c) c').π (op (Pairwise.pair i j)) =
    NatTrans.app ((fun c => coneEquivInverseObj F U c) c).π (op (Pairwise.pair i j))
[PROOFSTEP]
dsimp
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ f.Hom ≫ NatTrans.app c'.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j) =
    NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (i, j)
[PROOFSTEP]
rw [← f.w WalkingParallelPair.one, Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫
      NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π j =
    NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π j
[PROOFSTEP]
induction j using Opposite.rec' with
| h j => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫
      NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π j =
    NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π j
[PROOFSTEP]
induction j using Opposite.rec' with
| h j => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : CategoryTheory.Pairwise ι
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫
      NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π (op j) =
    NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π (op j)
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝ : ι
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫
      NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π (op (single a✝)) =
    NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π (op (single a✝))
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝ : ι
⊢ 𝟙 c.pt ≫ (Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫ Pi.π (fun i => F.obj (op (U i))) a✝ =
    NatTrans.app c.π (op (single a✝))
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝¹ a✝ : ι
⊢ 𝟙 ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).pt ≫
      NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π (op (Pairwise.pair a✝¹ a✝)) =
    NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π (op (Pairwise.pair a✝¹ a✝))
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝¹ a✝ : ι
⊢ 𝟙 c.pt ≫
      (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
        Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝) =
    NatTrans.app c.π (op (Pairwise.pair a✝¹ a✝))
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫
      NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π j =
    NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π j
[PROOFSTEP]
induction j using Opposite.rec' with
| h j => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫
      NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π j =
    NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π j
[PROOFSTEP]
induction j using Opposite.rec' with
| h j => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
j : CategoryTheory.Pairwise ι
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫
      NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π (op j) =
    NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π (op j)
[PROOFSTEP]
rcases j with ⟨⟩
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝ : ι
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫
      NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π (op (single a✝)) =
    NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π (op (single a✝))
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝ : ι
⊢ 𝟙 c.pt ≫ NatTrans.app c.π (op (single a✝)) =
    (Pi.lift fun i => NatTrans.app c.π (op (single i))) ≫ Pi.π (fun i => F.obj (op (U i))) a✝
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝¹ a✝ : ι
⊢ 𝟙 ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).pt ≫
      NatTrans.app ((𝟭 (Cone ((diagram U).op ⋙ F))).obj c).π (op (Pairwise.pair a✝¹ a✝)) =
    NatTrans.app ((coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c).π (op (Pairwise.pair a✝¹ a✝))
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
a✝¹ a✝ : ι
⊢ 𝟙 c.pt ≫ NatTrans.app c.π (op (Pairwise.pair a✝¹ a✝)) =
    (Pi.lift fun b => NatTrans.app c.π (op (Pairwise.pair b.fst b.snd))) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝)
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ ∀ (j : WalkingParallelPair),
    𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt ≫
        NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π j =
      NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π j
[PROOFSTEP]
rintro ⟨_ | _⟩
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt ≫
      NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.zero =
    NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.zero
[PROOFSTEP]
refine limit.hom_ext fun ⟨j⟩ => ?_
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete ι
j : ι
⊢ (𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt ≫
        NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j } =
    NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.zero ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j }
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete ι
j : ι
⊢ (𝟙 c.pt ≫ Fork.ι c) ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j } =
    (Pi.lift fun i => Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j }
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt ≫
      NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.one =
    NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.one
[PROOFSTEP]
refine limit.hom_ext fun ⟨i, j⟩ => ?_
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt ≫
        NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.one ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 c.pt ≫ NatTrans.app c.π WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    (Pi.lift fun b =>
        NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (b.fst, b.snd)) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ ∀ (j : WalkingParallelPair),
    𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt ≫
        NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π j =
      NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π j
[PROOFSTEP]
rintro ⟨_ | _⟩
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt ≫
      NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.zero =
    NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.zero
[PROOFSTEP]
refine limit.hom_ext fun ⟨j⟩ => ?_
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete ι
j : ι
⊢ (𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt ≫
        NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j } =
    NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.zero ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j }
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete ι
j : ι
⊢ (𝟙 c.pt ≫ Pi.lift fun i => Fork.ι c ≫ Pi.π (fun i => F.obj (op (U i))) i) ≫
      limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j } =
    Fork.ι c ≫ limit.π (Discrete.functor fun i => F.obj (op (U i))) { as := j }
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt ≫
      NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.one =
    NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.one
[PROOFSTEP]
refine limit.hom_ext fun ⟨i, j⟩ => ?_
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt ≫
        NatTrans.app ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    NatTrans.app ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π WalkingParallelPair.one ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
dsimp [coneEquivInverse]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 c.pt ≫
        Pi.lift fun b =>
          NatTrans.app c.π WalkingParallelPair.one ≫ Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (b.fst, b.snd)) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    NatTrans.app c.π WalkingParallelPair.one ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ (coneEquivInverse F U ⋙ coneEquivFunctor F U).map f ≫
      ((fun c =>
            Iso.mk (ConeMorphism.mk (𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt))
              (ConeMorphism.mk (𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt)))
          d).hom =
    ((fun c =>
            Iso.mk (ConeMorphism.mk (𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt))
              (ConeMorphism.mk (𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt)))
          c).hom ≫
      (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).map f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ ((coneEquivInverse F U ⋙ coneEquivFunctor F U).map f ≫
        ((fun c =>
              Iso.mk (ConeMorphism.mk (𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt))
                (ConeMorphism.mk (𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt)))
            d).hom).Hom =
    (((fun c =>
              Iso.mk (ConeMorphism.mk (𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt))
                (ConeMorphism.mk (𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt)))
            c).hom ≫
        (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).map f).Hom
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ f.Hom ≫ 𝟙 d.pt = 𝟙 c.pt ≫ f.Hom
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    𝟙 ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
        NatTrans.app (F.mapCone (Cocone.op (cocone U))).π j =
      NatTrans.app
        ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π j
[PROOFSTEP]
intro x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      NatTrans.app (F.mapCone (Cocone.op (cocone U))).π x =
    NatTrans.app
      ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π x
[PROOFSTEP]
induction x with
| h x => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      NatTrans.app (F.mapCone (Cocone.op (cocone U))).π x =
    NatTrans.app
      ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π x
[PROOFSTEP]
induction x with
| h x => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
⊢ 𝟙 ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      NatTrans.app (F.mapCone (Cocone.op (cocone U))).π (op x) =
    NatTrans.app
      ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π
      (op x)
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      NatTrans.app (F.mapCone (Cocone.op (cocone U))).π (op (single a✝)) =
    NatTrans.app
      ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π
      (op (single a✝))
[PROOFSTEP]
simp
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ F.map (coconeιApp U (single a✝)).op = F.map (leSupr U a✝).op
[PROOFSTEP]
rfl
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ 𝟙 ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).pt ≫
      NatTrans.app (F.mapCone (Cocone.op (cocone U))).π (op (Pairwise.pair a✝¹ a✝)) =
    NatTrans.app
      ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π
      (op (Pairwise.pair a✝¹ a✝))
[PROOFSTEP]
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res, SheafConditionEqualizerProducts.leftRes]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ 𝟙 (F.obj (op (iSup U))) ≫ F.map (coconeιApp U (Pairwise.pair a✝¹ a✝)).op =
    ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝)
[PROOFSTEP]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ F.map (coconeιApp U (Pairwise.pair a✝¹ a✝)).op = F.map (leSupr U a✝¹).op ≫ F.map (infLELeft (U a✝¹) (U a✝)).op
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ F.map (coconeιApp U (Pairwise.pair a✝¹ a✝)).op = F.map ((leSupr U a✝¹).op ≫ (infLELeft (U a✝¹) (U a✝)).op)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    𝟙 (F.mapCone (Cocone.op (cocone U))).pt ≫
        NatTrans.app
          ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π
          j =
      NatTrans.app (F.mapCone (Cocone.op (cocone U))).π j
[PROOFSTEP]
intro x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 (F.mapCone (Cocone.op (cocone U))).pt ≫
      NatTrans.app
        ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π x =
    NatTrans.app (F.mapCone (Cocone.op (cocone U))).π x
[PROOFSTEP]
induction x with
| h x => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ 𝟙 (F.mapCone (Cocone.op (cocone U))).pt ≫
      NatTrans.app
        ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π x =
    NatTrans.app (F.mapCone (Cocone.op (cocone U))).π x
[PROOFSTEP]
induction x with
| h x => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
x : CategoryTheory.Pairwise ι
⊢ 𝟙 (F.mapCone (Cocone.op (cocone U))).pt ≫
      NatTrans.app
        ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π
        (op x) =
    NatTrans.app (F.mapCone (Cocone.op (cocone U))).π (op x)
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ 𝟙 (F.mapCone (Cocone.op (cocone U))).pt ≫
      NatTrans.app
        ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π
        (op (single a✝)) =
    NatTrans.app (F.mapCone (Cocone.op (cocone U))).π (op (single a✝))
[PROOFSTEP]
simp
[GOAL]
case h.single
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝ : ι
⊢ F.map (leSupr U a✝).op = F.map (coconeιApp U (single a✝)).op
[PROOFSTEP]
rfl
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ 𝟙 (F.mapCone (Cocone.op (cocone U))).pt ≫
      NatTrans.app
        ((CategoryTheory.Equivalence.symm (coneEquiv F U)).functor.obj (SheafConditionEqualizerProducts.fork F U)).π
        (op (Pairwise.pair a✝¹ a✝)) =
    NatTrans.app (F.mapCone (Cocone.op (cocone U))).π (op (Pairwise.pair a✝¹ a✝))
[PROOFSTEP]
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res, SheafConditionEqualizerProducts.leftRes]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ 𝟙 (F.obj (op (iSup U))) ≫
      ((Pi.lift fun i => F.map (leSupr U i).op) ≫
          Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
        Pi.π (fun p => F.obj (op (U p.fst ⊓ U p.snd))) (a✝¹, a✝) =
    F.map (coconeιApp U (Pairwise.pair a✝¹ a✝)).op
[PROOFSTEP]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ F.map (leSupr U a✝¹).op ≫ F.map (infLELeft (U a✝¹) (U a✝)).op = F.map (coconeιApp U (Pairwise.pair a✝¹ a✝)).op
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
case h.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ F.map ((leSupr U a✝¹).op ≫ (infLELeft (U a✝¹) (U a✝)).op) = F.map (coconeιApp U (Pairwise.pair a✝¹ a✝)).op
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ ∀ (j : WalkingParallelPair),
    𝟙 ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).pt ≫
        NatTrans.app (SheafConditionEqualizerProducts.fork F U).π j =
      NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ 𝟙 ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).pt ≫
      NatTrans.app (SheafConditionEqualizerProducts.fork F U).π WalkingParallelPair.zero =
    NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ SheafConditionEqualizerProducts.res F U = Pi.lift fun i => F.map (coconeιApp U (single i)).op
[PROOFSTEP]
rfl
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ 𝟙 ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).pt ≫
      NatTrans.app (SheafConditionEqualizerProducts.fork F U).π WalkingParallelPair.one =
    NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π WalkingParallelPair.one
[PROOFSTEP]
refine limit.hom_ext fun ⟨i, j⟩ => ?_
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).pt ≫
        NatTrans.app (SheafConditionEqualizerProducts.fork F U).π WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π WalkingParallelPair.one ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res, SheafConditionEqualizerProducts.leftRes]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 (F.obj (op (iSup U))) ≫
        (Pi.lift fun i => F.map (leSupr U i).op) ≫
          Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    (Pi.lift fun b => F.map (coconeιApp U (Pairwise.pair b.fst b.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ F.map (leSupr U i).op ≫ F.map (infLELeft (U i) (U j)).op = F.map (coconeιApp U (Pairwise.pair i j)).op
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ F.map ((leSupr U i).op ≫ (infLELeft (U i) (U j)).op) = F.map (coconeιApp U (Pairwise.pair i j)).op
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ ∀ (j : WalkingParallelPair),
    𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
        NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π j =
      NatTrans.app (SheafConditionEqualizerProducts.fork F U).π j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ 𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
      NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π WalkingParallelPair.zero =
    NatTrans.app (SheafConditionEqualizerProducts.fork F U).π WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ (Pi.lift fun i => F.map (coconeιApp U (single i)).op) = SheafConditionEqualizerProducts.res F U
[PROOFSTEP]
rfl
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
⊢ 𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
      NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π WalkingParallelPair.one =
    NatTrans.app (SheafConditionEqualizerProducts.fork F U).π WalkingParallelPair.one
[PROOFSTEP]
refine limit.hom_ext fun ⟨i, j⟩ => ?_
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
        NatTrans.app ((coneEquiv F U).functor.obj (F.mapCone (Cocone.op (cocone U)))).π WalkingParallelPair.one) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    NatTrans.app (SheafConditionEqualizerProducts.fork F U).π WalkingParallelPair.one ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res, SheafConditionEqualizerProducts.leftRes]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ (𝟙 (F.obj (op (iSup U))) ≫ Pi.lift fun b => F.map (coconeιApp U (Pairwise.pair b.fst b.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) } =
    ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (op (U p.fst ⊓ U p.snd))) { as := (i, j) }
[PROOFSTEP]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ F.map (coconeιApp U (Pairwise.pair i j)).op = F.map (leSupr U i).op ≫ F.map (infLELeft (U i) (U j)).op
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (F.mapCone (Cocone.op (cocone U)))
x✝ : Discrete (ι × ι)
i j : ι
⊢ F.map (coconeιApp U (Pairwise.pair i j)).op = F.map ((leSupr U i).op ≫ (infLELeft (U i) (U j)).op)
[PROOFSTEP]
rfl
