C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ IsSheafEqualizerProducts F ↔ IsSheafEqualizerProducts (F ⋙ G)
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ IsSheaf F ↔ IsSheaf (F ⋙ G)
rw [Presheaf.isSheaf_iff_isSheafEqualizerProducts,
  Presheaf.isSheaf_iff_isSheafEqualizerProducts]
case mp
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ IsSheafEqualizerProducts F → IsSheafEqualizerProducts (F ⋙ G)

case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ IsSheafEqualizerProducts (F ⋙ G) → IsSheafEqualizerProducts F
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ IsSheafEqualizerProducts F ↔ IsSheafEqualizerProducts (F ⋙ G)
constructor
case mp
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
case mp
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ IsSheafEqualizerProducts F → IsSheafEqualizerProducts (F ⋙ G)
intro S ι U
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
case mp
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
obtain ⟨t₁⟩ := S U
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
letI := preservesSmallestLimitsOfPreservesLimits G
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
t₂ : IsLimit (G.mapCone (fork F U))
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
have t₂ := @PreservesLimit.preserves _ _ _ _ _ _ _ G _ _ t₁
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
t₂ : IsLimit (G.mapCone (fork F U))
t₃ : IsLimit ((Cones.postcompose (diagramCompPreservesLimits G F U).inv).obj (fork (F ⋙ G) U))
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
t₂ : IsLimit (G.mapCone (fork F U))
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
have t₃ := IsLimit.ofIsoLimit t₂ (mapConeFork G F U)
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
t₂ : IsLimit (G.mapCone (fork F U))
t₃ : IsLimit ((Cones.postcompose (diagramCompPreservesLimits G F U).inv).obj (fork (F ⋙ G) U))
t₄ : (fun x => IsLimit (fork (F ⋙ G) U)) t₃
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
t₂ : IsLimit (G.mapCone (fork F U))
t₃ : IsLimit ((Cones.postcompose (diagramCompPreservesLimits G F U).inv).obj (fork (F ⋙ G) U))
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
have t₄ := IsLimit.postcomposeInvEquiv _ _ t₃
no goals
case mp.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts F
ι : Type v
U : ι → Opens ↑X
t₁ : IsLimit (fork F U)
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
t₂ : IsLimit (G.mapCone (fork F U))
t₃ : IsLimit ((Cones.postcompose (diagramCompPreservesLimits G F U).inv).obj (fork (F ⋙ G) U))
t₄ : (fun x => IsLimit (fork (F ⋙ G) U)) t₃
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
exact ⟨t₄⟩
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (fork F U))
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
⊢ IsSheafEqualizerProducts (F ⋙ G) → IsSheafEqualizerProducts F
intro S ι U
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
⊢ IsLimit (fork F U)
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (fork F U))
refine' ⟨_⟩
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
⊢ IsLimit (fork F U)
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
⊢ IsLimit (fork F U)
let f := equalizer.lift _ (w F U)
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this : IsIso (G.map f)
⊢ IsLimit (fork F U)
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this : IsIso (G.map f)
⊢ IsLimit (fork F U)
skip
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ IsLimit (fork F U)
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this : IsIso (G.map f)
⊢ IsLimit (fork F U)
haveI : IsIso f := isIso_of_reflects_iso f G
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ limit.cone (parallelPair (leftRes F U) (rightRes F U)) ≅ fork F U
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ IsLimit (fork F U)
apply IsLimit.ofIsoLimit (limit.isLimit _)
case I
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ fork F U ≅ limit.cone (parallelPair (leftRes F U) (rightRes F U))
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ limit.cone (parallelPair (leftRes F U) (rightRes F U)) ≅ fork F U
apply Iso.symm
case I.φ
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ (fork F U).pt ≅ (limit.cone (parallelPair (leftRes F U) (rightRes F U))).pt

case I.w
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ autoParam
    (∀ (j : WalkingParallelPair),
      (fork F U).π.app j = ?I.φ.hom ≫ (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π.app j)
    _auto✝
case I
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ fork F U ≅ limit.cone (parallelPair (leftRes F U) (rightRes F U))
fapply Cones.ext
case I.w
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ autoParam
    (∀ (j : WalkingParallelPair),
      (fork F U).π.app j = (asIso f).hom ≫ (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π.app j)
    _auto✝
case I.φ
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ (fork F U).pt ≅ (limit.cone (parallelPair (leftRes F U) (rightRes F U))).pt

case I.w
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ autoParam
    (∀ (j : WalkingParallelPair),
      (fork F U).π.app j = ?I.φ.hom ≫ (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π.app j)
    _auto✝
exact asIso f
no goals
case I.w.one
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
this✝ : IsIso (G.map f)
this : IsIso f
⊢ (fork F U).π.app WalkingParallelPair.one =
    (asIso f).hom ≫ (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π.app WalkingParallelPair.one
simp
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
⊢ IsIso (G.map f)
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
⊢ IsIso (G.map f)
let c := fork (F ⋙ G) U
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
⊢ IsIso (G.map f)
case mpr
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
⊢ IsIso (G.map f)
obtain ⟨hc⟩ := S U
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
⊢ IsIso (G.map f)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
⊢ IsIso (G.map f)
let d := G.mapCone (equalizer.fork (leftRes.{v} F U) (rightRes F U))
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
⊢ IsIso (G.map f)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
⊢ IsIso (G.map f)
letI := preservesSmallestLimitsOfPreservesLimits G
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
⊢ IsIso (G.map f)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
⊢ IsIso (G.map f)
have hd : IsLimit d := PreservesLimit.preserves (limit.isLimit _)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
⊢ IsIso (G.map f)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
⊢ IsIso (G.map f)
let d' := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
⊢ IsIso (G.map f)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
⊢ IsIso (G.map f)
have hd' : IsLimit d' :=
  (IsLimit.postcomposeHomEquiv (diagramCompPreservesLimits G F U : _) d).symm hd
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
f' : c ⟶ d' := Fork.mkHom (G.map f) (_ : G.map f ≫ Fork.ι d' = Fork.ι c)
⊢ IsIso (G.map f)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
⊢ IsIso (G.map f)
let f' : c ⟶ d' := Fork.mkHom (G.map f) (by
  dsimp only [diagramCompPreservesLimits, res]
  dsimp only [Fork.ι]
  refine limit.hom_ext fun j => ?_
  dsimp
  simp only [Category.assoc, ← Functor.map_comp_assoc, equalizer.lift_ι,
    map_lift_piComparison_assoc]
  dsimp [res])
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this✝ : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
f' : c ⟶ d' := Fork.mkHom (G.map f) (_ : G.map f ≫ Fork.ι d' = Fork.ι c)
this : IsIso f'
⊢ IsIso (G.map f)
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
f' : c ⟶ d' := Fork.mkHom (G.map f) (_ : G.map f ≫ Fork.ι d' = Fork.ι c)
⊢ IsIso (G.map f)
haveI : IsIso f' := IsLimit.hom_isIso hc hd' f'
no goals
case mpr.intro
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this✝ : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
f' : c ⟶ d' := Fork.mkHom (G.map f) (_ : G.map f ≫ Fork.ι d' = Fork.ι c)
this : IsIso f'
⊢ IsIso (G.map f)
exact IsIso.of_iso ((Cones.forget _).mapIso (asIso f'))
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
⊢ G.map
        (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
          (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
      Fork.ι
        ((Cones.postcompose
              (NatIso.ofComponents fun X_1 =>
                  WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (U i).op)
                    (PreservesProduct.iso G fun p => F.obj (U p.fst ⊓ U p.snd).op) X_1).hom).obj
          (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))) =
    Fork.ι (fork (F ⋙ G) U)
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
⊢ G.map f ≫ Fork.ι d' = Fork.ι c
dsimp only [diagramCompPreservesLimits, res]
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
⊢ G.map
        (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
          (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
      ((Cones.postcompose
                  (NatIso.ofComponents fun X_1 =>
                      WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (U i).op)
                        (PreservesProduct.iso G fun p => F.obj (U p.fst ⊓ U p.snd).op) X_1).hom).obj
              (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))).π.app
        WalkingParallelPair.zero =
    (fork (F ⋙ G) U).π.app WalkingParallelPair.zero
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
⊢ G.map
        (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
          (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
      Fork.ι
        ((Cones.postcompose
              (NatIso.ofComponents fun X_1 =>
                  WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (U i).op)
                    (PreservesProduct.iso G fun p => F.obj (U p.fst ⊓ U p.snd).op) X_1).hom).obj
          (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))) =
    Fork.ι (fork (F ⋙ G) U)
dsimp only [Fork.ι]
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
j : Discrete ι
⊢ (G.map
          (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
            (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
        ((Cones.postcompose
                    (NatIso.ofComponents fun X_1 =>
                        WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (U i).op)
                          (PreservesProduct.iso G fun p => F.obj (U p.fst ⊓ U p.snd).op) X_1).hom).obj
                (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))).π.app
          WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => (F ⋙ G).obj (U i).op) j =
    (fork (F ⋙ G) U).π.app WalkingParallelPair.zero ≫ limit.π (Discrete.functor fun i => (F ⋙ G).obj (U i).op) j
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
⊢ G.map
        (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
          (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
      ((Cones.postcompose
                  (NatIso.ofComponents fun X_1 =>
                      WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (U i).op)
                        (PreservesProduct.iso G fun p => F.obj (U p.fst ⊓ U p.snd).op) X_1).hom).obj
              (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))).π.app
        WalkingParallelPair.zero =
    (fork (F ⋙ G) U).π.app WalkingParallelPair.zero
refine limit.hom_ext fun j => ?_
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
j : Discrete ι
⊢ (G.map
          (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
            (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
        G.map (equalizer.ι (leftRes F U) (rightRes F U)) ≫ piComparison G fun i => F.obj (U i).op) ≫
      limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j =
    res (F ⋙ G) U ≫ limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
j : Discrete ι
⊢ (G.map
          (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
            (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
        ((Cones.postcompose
                    (NatIso.ofComponents fun X_1 =>
                        WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (U i).op)
                          (PreservesProduct.iso G fun p => F.obj (U p.fst ⊓ U p.snd).op) X_1).hom).obj
                (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))).π.app
          WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => (F ⋙ G).obj (U i).op) j =
    (fork (F ⋙ G) U).π.app WalkingParallelPair.zero ≫ limit.π (Discrete.functor fun i => (F ⋙ G).obj (U i).op) j
dsimp
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
j : Discrete ι
⊢ (Pi.lift fun j => G.map (F.map (Opens.leSupr U j).op)) ≫
      limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j =
    res (F ⋙ G) U ≫ limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
j : Discrete ι
⊢ (G.map
          (equalizer.lift (Pi.lift fun i => F.map (Opens.leSupr U i).op)
            (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)) ≫
        G.map (equalizer.ι (leftRes F U) (rightRes F U)) ≫ piComparison G fun i => F.obj (U i).op) ≫
      limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j =
    res (F ⋙ G) U ≫ limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j
simp only [Category.assoc, ← Functor.map_comp_assoc, equalizer.lift_ι,
  map_lift_piComparison_assoc]
no goals
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasLimits C
inst✝¹ : HasLimits D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
S : IsSheafEqualizerProducts (F ⋙ G)
ι : Type v
U : ι → Opens ↑X
f : F.obj (iSup U).op ⟶ equalizer (leftRes F U) (rightRes F U) :=
  equalizer.lift (res F U) (_ : res F U ≫ leftRes F U = res F U ≫ rightRes F U)
c : Fork (leftRes (F ⋙ G) U) (rightRes (F ⋙ G) U) := fork (F ⋙ G) U
hc : IsLimit (fork (F ⋙ G) U)
d : Cone (parallelPair (leftRes F U) (rightRes F U) ⋙ G) := G.mapCone (equalizer.fork (leftRes F U) (rightRes F U))
this : PreservesLimitsOfSize G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
d' : Cone (diagram (F ⋙ G) U) := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
hd' : IsLimit d'
j : Discrete ι
⊢ (Pi.lift fun j => G.map (F.map (Opens.leSupr U j).op)) ≫
      limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j =
    res (F ⋙ G) U ≫ limit.π (Discrete.functor fun i => G.obj (F.obj (U i).op)) j
dsimp [res]