[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ diagram F U ⋙ G ≅ diagram (F ⋙ G) U
[PROOFSTEP]
fapply NatIso.ofComponents
[GOAL]
case app
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (X_1 : WalkingParallelPair) → (diagram F U ⋙ G).obj X_1 ≅ (diagram (F ⋙ G) U).obj X_1
case naturality
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ autoParam
    (∀ {X_1 Y : WalkingParallelPair} (f : X_1 ⟶ Y),
      (diagram F U ⋙ G).map f ≫ (?app Y).hom = (?app X_1).hom ≫ (diagram (F ⋙ G) U).map f)
    _auto✝
[PROOFSTEP]
rintro ⟨j⟩
[GOAL]
case app.zero
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (diagram F U ⋙ G).obj WalkingParallelPair.zero ≅ (diagram (F ⋙ G) U).obj WalkingParallelPair.zero
case app.one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (diagram F U ⋙ G).obj WalkingParallelPair.one ≅ (diagram (F ⋙ G) U).obj WalkingParallelPair.one
case naturality
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ autoParam
    (∀ {X_1 Y : WalkingParallelPair} (f : X_1 ⟶ Y),
      (diagram F U ⋙ G).map f ≫ (?m.6024 Y).hom = (?m.6024 X_1).hom ≫ (diagram (F ⋙ G) U).map f)
    _auto✝
[PROOFSTEP]
exact PreservesProduct.iso _ _
[GOAL]
case app.one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (diagram F U ⋙ G).obj WalkingParallelPair.one ≅ (diagram (F ⋙ G) U).obj WalkingParallelPair.one
case naturality
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ autoParam
    (∀ {X_1 Y : WalkingParallelPair} (f : X_1 ⟶ Y),
      (diagram F U ⋙ G).map f ≫ (?m.6024 Y).hom = (?m.6024 X_1).hom ≫ (diagram (F ⋙ G) U).map f)
    _auto✝
[PROOFSTEP]
exact PreservesProduct.iso _ _
[GOAL]
case naturality
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ autoParam
    (∀ {X_1 Y : WalkingParallelPair} (f : X_1 ⟶ Y),
      (diagram F U ⋙ G).map f ≫
          (WalkingParallelPair.casesOn Y (PreservesProduct.iso G fun i => F.obj (op (U i)))
              (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom =
        (WalkingParallelPair.casesOn X_1 (PreservesProduct.iso G fun i => F.obj (op (U i)))
              (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
          (diagram (F ⋙ G) U).map f)
    _auto✝
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case naturality.zero.zero.id
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (diagram F U ⋙ G).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
      (diagram (F ⋙ G) U).map (WalkingParallelPairHom.id WalkingParallelPair.zero)
[PROOFSTEP]
refine limit.hom_ext (fun j => ?_)
[GOAL]
case naturality.zero.zero.id
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete ι
⊢ ((diagram F U ⋙ G).map (WalkingParallelPairHom.id WalkingParallelPair.zero) ≫
        (WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom) ≫
      limit.π (Discrete.functor fun i => (F ⋙ G).obj (op (U i))) j =
    ((WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
        (diagram (F ⋙ G) U).map (WalkingParallelPairHom.id WalkingParallelPair.zero)) ≫
      limit.π (Discrete.functor fun i => (F ⋙ G).obj (op (U i))) j
[PROOFSTEP]
simp
[GOAL]
case naturality.zero.one.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (diagram F U ⋙ G).map WalkingParallelPairHom.left ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
      (diagram (F ⋙ G) U).map WalkingParallelPairHom.left
[PROOFSTEP]
refine
  limit.hom_ext
    (fun j => ?_)
      -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
[GOAL]
case naturality.zero.one.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ ((diagram F U ⋙ G).map WalkingParallelPairHom.left ≫
        (WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom) ≫
      limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j =
    ((WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
        (diagram (F ⋙ G) U).map WalkingParallelPairHom.left) ≫
      limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j
[PROOFSTEP]
dsimp [diagram, leftRes, rightRes]
[GOAL]
case naturality.zero.one.left
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ (G.map (Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (Opens.infLELeft (U p.fst) (U p.snd)).op) ≫
        piComparison G fun p => F.obj (op (U p.fst ⊓ U p.snd))) ≫
      limit.π (Discrete.functor fun p => G.obj (F.obj (op (U p.fst ⊓ U p.snd)))) j =
    ((piComparison G fun i => F.obj (op (U i))) ≫
        Pi.lift fun p =>
          Pi.π (fun i => G.obj (F.obj (op (U i)))) p.fst ≫ G.map (F.map (Opens.infLELeft (U p.fst) (U p.snd)).op)) ≫
      limit.π (Discrete.functor fun p => G.obj (F.obj (op (U p.fst ⊓ U p.snd)))) j
[PROOFSTEP]
simp [limit.lift_π, Functor.comp_map, map_lift_piComparison, Fan.mk_π_app, PreservesProduct.iso_hom,
  parallelPair_map_left, Functor.map_comp, Category.assoc]
[GOAL]
case naturality.zero.one.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (diagram F U ⋙ G).map WalkingParallelPairHom.right ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
      (diagram (F ⋙ G) U).map WalkingParallelPairHom.right
[PROOFSTEP]
refine
  limit.hom_ext
    (fun j => ?_)
      -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
[GOAL]
case naturality.zero.one.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ ((diagram F U ⋙ G).map WalkingParallelPairHom.right ≫
        (WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom) ≫
      limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j =
    ((WalkingParallelPair.casesOn WalkingParallelPair.zero (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
        (diagram (F ⋙ G) U).map WalkingParallelPairHom.right) ≫
      limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j
[PROOFSTEP]
dsimp [diagram, leftRes, rightRes]
[GOAL]
case naturality.zero.one.right
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ (G.map (Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.snd ≫ F.map (Opens.infLERight (U p.fst) (U p.snd)).op) ≫
        piComparison G fun p => F.obj (op (U p.fst ⊓ U p.snd))) ≫
      limit.π (Discrete.functor fun p => G.obj (F.obj (op (U p.fst ⊓ U p.snd)))) j =
    ((piComparison G fun i => F.obj (op (U i))) ≫
        Pi.lift fun p =>
          Pi.π (fun i => G.obj (F.obj (op (U i)))) p.snd ≫ G.map (F.map (Opens.infLERight (U p.fst) (U p.snd)).op)) ≫
      limit.π (Discrete.functor fun p => G.obj (F.obj (op (U p.fst ⊓ U p.snd)))) j
[PROOFSTEP]
simp [limit.lift_π, Functor.comp_map, map_lift_piComparison, Fan.mk_π_app, PreservesProduct.iso_hom,
  parallelPair_map_left, Functor.map_comp, Category.assoc]
[GOAL]
case naturality.one.one.id
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ (diagram F U ⋙ G).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
      (diagram (F ⋙ G) U).map (WalkingParallelPairHom.id WalkingParallelPair.one)
[PROOFSTEP]
refine limit.hom_ext (fun j => ?_)
[GOAL]
case naturality.one.one.id
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ ((diagram F U ⋙ G).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
        (WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom) ≫
      limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j =
    ((WalkingParallelPair.casesOn WalkingParallelPair.one (PreservesProduct.iso G fun i => F.obj (op (U i)))
            (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd)))).hom ≫
        (diagram (F ⋙ G) U).map (WalkingParallelPairHom.id WalkingParallelPair.one)) ≫
      limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j
[PROOFSTEP]
simp [diagram, leftRes, rightRes]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : WalkingParallelPair
⊢ NatTrans.app (G.mapCone (fork F U)).π j =
    (Iso.refl (G.mapCone (fork F U)).pt).hom ≫
      NatTrans.app ((Cones.postcompose (diagramCompPreservesLimits G F U).inv).obj (fork (F ⋙ G) U)).π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : WalkingParallelPair
⊢ G.map (NatTrans.app (fork F U).π j) =
    𝟙 (G.obj (F.obj (op (iSup U)))) ≫
      NatTrans.app (fork (F ⋙ G) U).π j ≫ NatTrans.app (diagramCompPreservesLimits G F U).inv j
[PROOFSTEP]
simp [diagramCompPreservesLimits]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : WalkingParallelPair
⊢ G.map (NatTrans.app (fork F U).π j) =
    NatTrans.app (fork (F ⋙ G) U).π j ≫
      (WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))) j).inv
[PROOFSTEP]
cases j
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ G.map (NatTrans.app (fork F U).π WalkingParallelPair.zero) =
    NatTrans.app (fork (F ⋙ G) U).π WalkingParallelPair.zero ≫
      (WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))) WalkingParallelPair.zero).inv
[PROOFSTEP]
dsimp
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ G.map (NatTrans.app (fork F U).π WalkingParallelPair.one) =
    NatTrans.app (fork (F ⋙ G) U).π WalkingParallelPair.one ≫
      (WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (op (U i)))
          (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))) WalkingParallelPair.one).inv
[PROOFSTEP]
dsimp
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ G.map (res F U) = res (F ⋙ G) U ≫ (PreservesProduct.iso G fun i => F.obj (op (U i))).inv
[PROOFSTEP]
rw [Iso.eq_comp_inv]
  -- Porting note : `ext` can't see `limit.hom_ext` applies here:
        -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ G.map (res F U) ≫ (PreservesProduct.iso G fun i => F.obj (op (U i))).hom = res (F ⋙ G) U
[PROOFSTEP]
refine
  limit.hom_ext
    (fun j => ?_)
      -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
[GOAL]
case zero
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete ι
⊢ (G.map (res F U) ≫ (PreservesProduct.iso G fun i => F.obj (op (U i))).hom) ≫
      limit.π (Discrete.functor fun i => (F ⋙ G).obj (op (U i))) j =
    res (F ⋙ G) U ≫ limit.π (Discrete.functor fun i => (F ⋙ G).obj (op (U i))) j
[PROOFSTEP]
simp [diagram, leftRes, rightRes, res]
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ G.map (res F U ≫ leftRes F U) =
    (res (F ⋙ G) U ≫ leftRes (F ⋙ G) U) ≫ (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))).inv
[PROOFSTEP]
rw [Iso.eq_comp_inv]
  -- Porting note : `ext` can't see `limit.hom_ext` applies here:
        -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
⊢ G.map (res F U ≫ leftRes F U) ≫ (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))).hom =
    res (F ⋙ G) U ≫ leftRes (F ⋙ G) U
[PROOFSTEP]
refine
  limit.hom_ext
    (fun j => ?_)
      -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ (G.map (res F U ≫ leftRes F U) ≫ (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))).hom) ≫
      limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j =
    (res (F ⋙ G) U ≫ leftRes (F ⋙ G) U) ≫ limit.π (Discrete.functor fun p => (F ⋙ G).obj (op (U p.fst ⊓ U p.snd))) j
[PROOFSTEP]
dsimp [diagram, leftRes, rightRes, res]
  -- Porting note : there used to be a non-terminal `simp` for `squeeze_simp` did not work,
        -- however, `simp?` works fine now, but in both mathlib3 and mathlib4, two `simp`s are
        -- required to close goal
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ (G.map
          ((Pi.lift fun i => F.map (Opens.leSupr U i).op) ≫
            Pi.lift fun p => Pi.π (fun i => F.obj (op (U i))) p.fst ≫ F.map (Opens.infLELeft (U p.fst) (U p.snd)).op) ≫
        piComparison G fun p => F.obj (op (U p.fst ⊓ U p.snd))) ≫
      limit.π (Discrete.functor fun p => G.obj (F.obj (op (U p.fst ⊓ U p.snd)))) j =
    ((Pi.lift fun i => G.map (F.map (Opens.leSupr U i).op)) ≫
        Pi.lift fun p =>
          Pi.π (fun i => G.obj (F.obj (op (U i)))) p.fst ≫ G.map (F.map (Opens.infLELeft (U p.fst) (U p.snd)).op)) ≫
      limit.π (Discrete.functor fun p => G.obj (F.obj (op (U p.fst ⊓ U p.snd)))) j
[PROOFSTEP]
simp only [Functor.map_comp, Category.assoc, map_lift_piComparison, limit.lift_π, Fan.mk_pt, Fan.mk_π_app,
  limit.lift_π_assoc, Discrete.functor_obj]
[GOAL]
case one
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
inst✝³ : HasLimits C
D : Type u₂
inst✝² : Category.{v, u₂} D
inst✝¹ : HasLimits D
G : C ⥤ D
inst✝ : PreservesLimits G
X : TopCat
F : Presheaf C X
ι : Type v
U : ι → Opens ↑X
j : Discrete (ι × ι)
⊢ G.map (Pi.lift fun i => F.map (Opens.leSupr U i).op) ≫
      G.map (Pi.π (fun i => F.obj (op (U i))) j.as.fst) ≫ G.map (F.map (Opens.infLELeft (U j.as.fst) (U j.as.snd)).op) =
    G.map (F.map (Opens.leSupr U j.as.fst).op) ≫ G.map (F.map (Opens.infLELeft (U j.as.fst) (U j.as.snd)).op)
[PROOFSTEP]
simp only [limit.lift_π, Fan.mk_π_app, ← G.map_comp, limit.lift_π_assoc, Fan.mk_π_app]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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)
[PROOFSTEP]
rw [Presheaf.isSheaf_iff_isSheafEqualizerProducts, Presheaf.isSheaf_iff_isSheafEqualizerProducts]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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)
[PROOFSTEP]
intro S ι U
[GOAL]
case mp
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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))
[PROOFSTEP]
obtain ⟨t₁⟩ := S U
[GOAL]
case mp.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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))
[PROOFSTEP]
letI := preservesSmallestLimitsOfPreservesLimits G
[GOAL]
case mp.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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.{0, 0, v, v, u₁, u₂} G := preservesSmallestLimitsOfPreservesLimits G
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
[PROOFSTEP]
have t₂ := @PreservesLimit.preserves _ _ _ _ _ _ _ G _ _ t₁
[GOAL]
case mp.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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.{0, 0, v, v, u₁, u₂} G := preservesSmallestLimitsOfPreservesLimits G
t₂ : IsLimit (G.mapCone (fork F U))
⊢ Nonempty (IsLimit (fork (F ⋙ G) U))
[PROOFSTEP]
have t₃ :=
  IsLimit.ofIsoLimit t₂
    (mapConeFork G F U)
      -- and as postcomposing by a natural isomorphism preserves limit cones,
[GOAL]
case mp.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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.{0, 0, v, v, u₁, u₂} 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))
[PROOFSTEP]
have t₄ := IsLimit.postcomposeInvEquiv _ _ t₃
[GOAL]
case mp.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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.{0, 0, v, v, u₁, u₂} 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))
[PROOFSTEP]
exact ⟨t₄⟩
[GOAL]
case mpr
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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
[PROOFSTEP]
intro S ι U
[GOAL]
case mpr
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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))
[PROOFSTEP]
refine'
  ⟨_⟩
    -- Let `f` be the universal morphism from `F.obj U` to the equalizer
        -- of the sheaf condition fork, whatever it is.
        -- Our goal is to show that this is an isomorphism.
[GOAL]
case mpr
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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)
[PROOFSTEP]
let f :=
  equalizer.lift _
    (w F U)
      -- If we can do that,
[GOAL]
case mpr
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
suffices IsIso (G.map f)
  by
  skip
    -- we have that `f` itself is an isomorphism, since `G` reflects isomorphisms
  haveI : IsIso f := isIso_of_reflects_iso f G
  apply IsLimit.ofIsoLimit (limit.isLimit _)
  apply Iso.symm
  fapply Cones.ext
  exact asIso f
  rintro ⟨_ | _⟩ <;> · simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
skip
  -- we have that `f` itself is an isomorphism, since `G` reflects isomorphisms
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
haveI : IsIso f := isIso_of_reflects_iso f G
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
apply IsLimit.ofIsoLimit (limit.isLimit _)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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
[PROOFSTEP]
apply Iso.symm
[GOAL]
case I
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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))
[PROOFSTEP]
fapply Cones.ext
[GOAL]
case I.φ
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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),
      NatTrans.app (fork F U).π j =
        ?I.φ.hom ≫ NatTrans.app (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π j)
    _auto✝
[PROOFSTEP]
exact asIso f
[GOAL]
case I.w
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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),
      NatTrans.app (fork F U).π j =
        (asIso f).hom ≫ NatTrans.app (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π j)
    _auto✝
[PROOFSTEP]
rintro ⟨_ | _⟩
[GOAL]
case I.w.zero
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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
⊢ NatTrans.app (fork F U).π WalkingParallelPair.zero =
    (asIso f).hom ≫ NatTrans.app (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case I.w.one
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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
⊢ NatTrans.app (fork F U).π WalkingParallelPair.one =
    (asIso f).hom ≫ NatTrans.app (limit.cone (parallelPair (leftRes F U) (rightRes F U))).π WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
case mpr
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
let c := fork (F ⋙ G) U
[GOAL]
case mpr
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
obtain ⟨hc⟩ := S U
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
let d := G.mapCone (equalizer.fork (leftRes.{v} F U) (rightRes F U))
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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)
[PROOFSTEP]
letI := preservesSmallestLimitsOfPreservesLimits G
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} G := preservesSmallestLimitsOfPreservesLimits G
⊢ IsIso (G.map f)
[PROOFSTEP]
have hd : IsLimit d :=
  PreservesLimit.preserves
    (limit.isLimit _)
      -- Since both of these are limit cones
            -- (`c` by our hypothesis `S`, and `d` because `G` preserves limits),
            -- we hope to be able to conclude that `f` is an isomorphism.
            -- We say "not quite" above because `c` and `d` don't quite have the same shape:
            -- we need to postcompose by the natural isomorphism `diagramCompPreservesLimits`
            -- introduced above.
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} G := preservesSmallestLimitsOfPreservesLimits G
hd : IsLimit d
⊢ IsIso (G.map f)
[PROOFSTEP]
let d' := (Cones.postcompose (diagramCompPreservesLimits G F U).hom).obj d
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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)
[PROOFSTEP]
have hd' : IsLimit d' := (IsLimit.postcomposeHomEquiv (diagramCompPreservesLimits G F U : _) d).symm hd
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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)
[PROOFSTEP]
let f' : c ⟶ d' :=
  Fork.mkHom (G.map f)
    (by
      dsimp only [diagramCompPreservesLimits, res]
      dsimp only [Fork.ι]
        -- Porting note : `ext` can't see `limit.hom_ext` applies here:
                -- See https://github.com/leanprover-community/mathlib4/issues/5229
      refine limit.hom_ext fun j => ?_
      dsimp
      simp only [Category.assoc, ← Functor.map_comp_assoc, equalizer.lift_ι, map_lift_piComparison_assoc]
      dsimp [res])
      -- conclude that it is an isomorphism,
            -- just because it's a morphism between two limit cones.
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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
[PROOFSTEP]
dsimp only [diagramCompPreservesLimits, res]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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 (op (U i)))
                    (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))) X_1).hom).obj
          (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))) =
    Fork.ι (fork (F ⋙ G) U)
[PROOFSTEP]
dsimp only [Fork.ι]
  -- 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
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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)) ≫
      NatTrans.app
        ((Cones.postcompose
                (NatIso.ofComponents fun X_1 =>
                    WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (op (U i)))
                      (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))) X_1).hom).obj
            (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))).π
        WalkingParallelPair.zero =
    NatTrans.app (fork (F ⋙ G) U).π WalkingParallelPair.zero
[PROOFSTEP]
refine limit.hom_ext fun j => ?_
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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)) ≫
        NatTrans.app
          ((Cones.postcompose
                  (NatIso.ofComponents fun X_1 =>
                      WalkingParallelPair.rec (PreservesProduct.iso G fun i => F.obj (op (U i)))
                        (PreservesProduct.iso G fun p => F.obj (op (U p.fst ⊓ U p.snd))) X_1).hom).obj
              (G.mapCone (equalizer.fork (leftRes F U) (rightRes F U)))).π
          WalkingParallelPair.zero) ≫
      limit.π (Discrete.functor fun i => (F ⋙ G).obj (op (U i))) j =
    NatTrans.app (fork (F ⋙ G) U).π WalkingParallelPair.zero ≫
      limit.π (Discrete.functor fun i => (F ⋙ G).obj (op (U i))) j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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 (op (U i))) ≫
      limit.π (Discrete.functor fun i => G.obj (F.obj (op (U i)))) j =
    res (F ⋙ G) U ≫ limit.π (Discrete.functor fun i => G.obj (F.obj (op (U i)))) j
[PROOFSTEP]
simp only [Category.assoc, ← Functor.map_comp_assoc, equalizer.lift_ι, map_lift_piComparison_assoc]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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 (op (U i)))) j =
    res (F ⋙ G) U ≫ limit.π (Discrete.functor fun i => G.obj (F.obj (op (U i)))) j
[PROOFSTEP]
dsimp [res]
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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)
[PROOFSTEP]
haveI : IsIso f' := IsLimit.hom_isIso hc hd' f'
[GOAL]
case mpr.intro
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
D : Type u₂
inst✝⁴ : Category.{v, u₂} 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 (op (iSup U)) ⟶ 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.{0, 0, v, v, u₁, u₂} 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)
[PROOFSTEP]
exact IsIso.of_iso ((Cones.forget _).mapIso (asIso f'))
