C : Type u
inst✝¹ : Category 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 (U i).op) 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 (U i).op) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
C : Type u
inst✝¹ : Category 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
dsimp [res, leftRes, rightRes]
C : Type u
inst✝¹ : Category 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 (U i).op) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (U p.fst ⊓ U p.snd).op) x✝ =
    ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (U i).op) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (U p.fst ⊓ U p.snd).op) x✝
C : Type u
inst✝¹ : Category 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 (U i).op) 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 (U i).op) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op
refine limit.hom_ext (fun _ => ?_)
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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 (U i).op) p.fst ≫ F.map (infLELeft (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (U p.fst ⊓ U p.snd).op) x✝ =
    ((Pi.lift fun i => F.map (leSupr U i).op) ≫
        Pi.lift fun p => Pi.π (fun i => F.obj (U i).op) p.snd ≫ F.map (infLERight (U p.fst) (U p.snd)).op) ≫
      limit.π (Discrete.functor fun p => F.obj (U p.fst ⊓ U p.snd).op) x✝
simp only [limit.lift_π, limit.lift_π_assoc, Fan.mk_π_app, Category.assoc]
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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
rw [← F.map_comp]
C : Type u
inst✝¹ : Category 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)
C : Type u
inst✝¹ : Category 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
rw [← F.map_comp]
no goals
C : Type u
inst✝¹ : Category 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)
congr 1