[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      PrelocalPredicate.pred
        { pred := fun {U} => PrelocalPredicate.pred src✝,
          res :=
            (_ :
              ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
                PrelocalPredicate.pred src✝ f →
                  PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ PrelocalPredicate.pred
    { pred := fun {U} => PrelocalPredicate.pred src✝,
      res :=
        (_ :
          ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
            PrelocalPredicate.pred src✝ f →
              PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
    f
[PROOFSTEP]
apply continuous_iff_continuousAt.2
[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      PrelocalPredicate.pred
        { pred := fun {U} => PrelocalPredicate.pred src✝,
          res :=
            (_ :
              ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
                PrelocalPredicate.pred src✝ f →
                  PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∀ (x : { x // x ∈ U }), ContinuousAt f x
[PROOFSTEP]
intro x
[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      PrelocalPredicate.pred
        { pred := fun {U} => PrelocalPredicate.pred src✝,
          res :=
            (_ :
              ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
                PrelocalPredicate.pred src✝ f →
                  PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
x : { x // x ∈ U }
⊢ ContinuousAt f x
[PROOFSTEP]
specialize w x
[GOAL]
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
w :
  ∃ V x i,
    PrelocalPredicate.pred
      { pred := fun {U} => PrelocalPredicate.pred src✝,
        res :=
          (_ :
            ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
              PrelocalPredicate.pred src✝ f →
                PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
      fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ContinuousAt f x
[PROOFSTEP]
rcases w with ⟨V, m, i, w⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w :
  PrelocalPredicate.pred
    { pred := fun {U} => PrelocalPredicate.pred src✝,
      res :=
        (_ :
          ∀ {U V : Opens ↑X} (i : U ⟶ V) (f : { x // x ∈ V } → ↑T),
            PrelocalPredicate.pred src✝ f →
              PrelocalPredicate.pred src✝ fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
    fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ContinuousAt f x
[PROOFSTEP]
dsimp at w
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : Continuous fun x => f { val := ↑x, property := (_ : ↑x ∈ ↑U) }
⊢ ContinuousAt f x
[PROOFSTEP]
rw [continuous_iff_continuousAt] at w
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ∀ (x : { x // x ∈ V }), ContinuousAt (fun x => f { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x
⊢ ContinuousAt f x
[PROOFSTEP]
specialize w ⟨x, m⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ : ↑X → Type v
T : TopCat
src✝ : PrelocalPredicate fun x => ↑T := continuousPrelocal X T
U : Opens ↑X
f : { x // x ∈ U } → ↑T
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ContinuousAt (fun x => f { val := ↑x, property := (_ : ↑x ∈ ↑U) }) { val := ↑x, property := m }
⊢ ContinuousAt f x
[PROOFSTEP]
simpa using (Opens.openEmbedding_of_le i.le).continuousAt_iff.1 w
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
w :
  (fun {U} f =>
      ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
    f
x : { x // x ∈ V }
⊢ ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
specialize w (i x)
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ V }
w : ∃ V_1 x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
rcases w with ⟨V', m', i', p⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ V }
V' : Opens ↑X
m' : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x) ∈ V'
i' : V' ⟶ U
p : pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
refine' ⟨V ⊓ V', ⟨x.2, m'⟩, Opens.infLELeft _ _, _⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ V }
V' : Opens ↑X
m' : ↑((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x) ∈ V'
i' : V' ⟶ U
p : pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ pred P fun x =>
    (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
convert P.res (Opens.infLERight V V') _ p
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
w :
  ∀ (x : { x // x ∈ U }),
    ∃ V x i,
      pred
        {
          pred := fun {U} f =>
            ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x),
          res :=
            (_ :
              ∀ {V U : Opens ↑X} (i : V ⟶ U) (f : (x : { x // x ∈ U }) → T ↑x),
                (∀ (x : { x // x ∈ U }),
                    ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
                  ∀ (x : { x // x ∈ V }),
                    ∃ V_1 x i_1,
                      pred P fun x =>
                        (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
                          ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
x : { x // x ∈ U }
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
specialize w x
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
w :
  ∃ V x i,
    pred
      {
        pred := fun {U} f =>
          ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x),
        res :=
          (_ :
            ∀ {V U : Opens ↑X} (i : V ⟶ U) (f : (x : { x // x ∈ U }) → T ↑x),
              (∀ (x : { x // x ∈ U }),
                  ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
                ∀ (x : { x // x ∈ V }),
                  ∃ V_1 x i_1,
                    pred P fun x =>
                      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
                        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
      fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
rcases w with ⟨V, m, i, p⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p :
  pred
    {
      pred := fun {U} f =>
        ∀ (x : { x // x ∈ U }), ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x),
      res :=
        (_ :
          ∀ {V U : Opens ↑X} (i : V ⟶ U) (f : (x : { x // x ∈ U }) → T ↑x),
            (∀ (x : { x // x ∈ U }),
                ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
              ∀ (x : { x // x ∈ V }),
                ∃ V_1 x i_1,
                  pred P fun x =>
                    (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
                      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) }
    fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
specialize p ⟨x.1, m⟩
[GOAL]
case intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p :
  ∃ V_1 x i_1,
    pred P fun x =>
      (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
        ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
rcases p with ⟨V', m', i', p'⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
x : { x // x ∈ U }
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
V' : Opens ↑X
m' : ↑{ val := ↑x, property := m } ∈ V'
i' : V' ⟶ V
p' :
  pred P fun x =>
    (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x))
      ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
⊢ ∃ V x i, pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
exact ⟨V', m', i' ≫ i, p'⟩
[GOAL]
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
h : pred P f
x : { x // x ∈ U }
⊢ pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
[PROOFSTEP]
convert h
[GOAL]
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
let sf' : ∀ i : ι, (presheafToTypes X T).obj (op (U i)) := fun i => (sf i).val
[GOAL]
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
have sf'_comp : (presheafToTypes X T).IsCompatible U sf' := fun i j =>
  congr_arg Subtype.val
    (sf_comp i j)
      -- So, we can obtain a unique gluing
[GOAL]
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
obtain ⟨gl, gl_spec, gl_uniq⟩ := (sheafToTypes X T).existsUnique_gluing U sf' sf'_comp
[GOAL]
case intro.intro
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∃! s, IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s
[PROOFSTEP]
refine' ⟨⟨gl, _⟩, _, _⟩
[GOAL]
case intro.intro.refine'_1
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ PrelocalPredicate.pred P.toPrelocalPredicate gl
[PROOFSTEP]
apply P.locality
[GOAL]
case intro.intro.refine'_1.x
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (x : { x // x ∈ (op (iSup U)).unop }),
    ∃ V x i,
      PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
        gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
rintro
  ⟨x, mem⟩
      -- Once we're at a particular point `x`, we can select some open set `x ∈ U i`.
[GOAL]
case intro.intro.refine'_1.x.mk
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
choose i hi using Opens.mem_iSup.mp mem
[GOAL]
case intro.intro.refine'_1.x.mk
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
i : ι
hi : x ∈ U i
⊢ ∃ V x i,
    PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
      gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
use U i, hi, Opens.leSupr U i
[GOAL]
case h
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
i : ι
hi : x ∈ U i
⊢ PrelocalPredicate.pred P.toPrelocalPredicate fun x =>
    gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)
[PROOFSTEP]
convert (sf i).property using 1
[GOAL]
case h.e'_5.h
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ (op (iSup U)).unop
i : ι
hi : x ∈ U i
e_4✝ : U i = (op (U i)).unop
⊢ (fun x => gl ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(op (iSup U)).unop) }) x)) = ↑(sf i)
[PROOFSTEP]
exact gl_spec i
[GOAL]
case intro.intro.refine'_2
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ (fun s => IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s)
    { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
exact fun i => Subtype.ext (gl_spec i)
[GOAL]
case intro.intro.refine'_3
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
⊢ ∀ (y : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))),
    (fun s => IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf s) y →
      y = { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
intro gl' hgl'
[GOAL]
case intro.intro.refine'_3
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ gl' = { val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
refine Subtype.ext ?_
[GOAL]
case intro.intro.refine'_3
X : TopCat
T : ↑X → Type v
P✝ : PrelocalPredicate T
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : IsCompatible (subpresheafToTypes P.toPrelocalPredicate) U sf
sf' : (i : ι) → (presheafToTypes X T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : IsCompatible (presheafToTypes X T) U sf'
gl : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))
gl_spec : IsGluing (sheafToTypes X T).val U sf' gl
gl_uniq :
  ∀ (y : (forget (Type v)).obj ((sheafToTypes X T).val.obj (op (iSup U)))),
    (fun s => IsGluing (sheafToTypes X T).val U sf' s) y → y = gl
gl' : (forget (Type v)).obj ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : IsGluing (subpresheafToTypes P.toPrelocalPredicate) U sf gl'
⊢ ↑gl' = ↑{ val := gl, property := (_ : PrelocalPredicate.pred P.toPrelocalPredicate gl) }
[PROOFSTEP]
exact gl_uniq gl'.1 fun i => congr_arg Subtype.val (hgl' i)
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
⊢ Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x ⟶ T x
[PROOFSTEP]
refine'
  colimit.desc _
    { pt := T x
      ι :=
        { app := fun U f => _
          naturality := _ } }
[GOAL]
case refine'_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
f :
  (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
        (Sheaf.presheaf (subsheafToTypes P))).obj
    U
⊢ ((Functor.const (OpenNhds x)ᵒᵖ).obj (T x)).obj U
[PROOFSTEP]
exact f.1 ⟨x, (unop U).2⟩
[GOAL]
case refine'_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
⊢ ∀ ⦃X_1 Y : (OpenNhds x)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
              (Sheaf.presheaf (subsheafToTypes P))).map
          f ≫
        (fun U f => ↑f { val := x, property := (_ : x ∈ U.unop.obj) }) Y =
      (fun U f => ↑f { val := x, property := (_ : x ∈ U.unop.obj) }) X_1 ≫
        ((Functor.const (OpenNhds x)ᵒᵖ).obj (T x)).map f
[PROOFSTEP]
aesop
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : { x // x ∈ U }
f : (Sheaf.presheaf (subsheafToTypes P)).obj (op U)
⊢ stalkToFiber P (↑x) (Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) x f) = ↑f x
[PROOFSTEP]
dsimp [Presheaf.germ, stalkToFiber]
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
x : { x // x ∈ U }
f : (Sheaf.presheaf (subsheafToTypes P)).obj (op U)
⊢ colimit.desc ((OpenNhds.inclusion ↑x).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑x, ι := NatTrans.mk fun U_1 f => ↑f { val := ↑x, property := (_ : ↑x ∈ U_1.unop.obj) } }
      (colimit.ι ((OpenNhds.inclusion ↑x).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
        (op { obj := U, property := (_ : ↑x ∈ U) }) f) =
    ↑f x
[PROOFSTEP]
cases x
[GOAL]
case mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
U : Opens ↑X
f : (Sheaf.presheaf (subsheafToTypes P)).obj (op U)
val✝ : ↑X
property✝ : val✝ ∈ U
⊢ colimit.desc
      ((OpenNhds.inclusion ↑{ val := val✝, property := property✝ }).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
      { pt := T ↑{ val := val✝, property := property✝ },
        ι :=
          NatTrans.mk fun U_1 f =>
            ↑f
              { val := ↑{ val := val✝, property := property✝ },
                property := (_ : ↑{ val := val✝, property := property✝ } ∈ U_1.unop.obj) } }
      (colimit.ι
        ((OpenNhds.inclusion ↑{ val := val✝, property := property✝ }).op ⋙ subpresheafToTypes P.toPrelocalPredicate)
        (op { obj := U, property := (_ : ↑{ val := val✝, property := property✝ } ∈ U) }) f) =
    ↑f { val := val✝, property := property✝ }
[PROOFSTEP]
simp
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
t : T x
⊢ ∃ a, stalkToFiber P x a = t
[PROOFSTEP]
rcases w t with ⟨U, f, h, rfl⟩
[GOAL]
case intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ ∃ a, stalkToFiber P x a = f { val := x, property := (_ : x ∈ U.obj) }
[PROOFSTEP]
fconstructor
[GOAL]
case intro.intro.intro.w
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
[PROOFSTEP]
exact (subsheafToTypes P).presheaf.germ ⟨x, U.2⟩ ⟨f, h⟩
[GOAL]
case intro.intro.intro.h
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f x_1, f { val := x, property := (_ : x ∈ U.obj) } = t
U : OpenNhds x
f : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y
h : PrelocalPredicate.pred P.toPrelocalPredicate f
⊢ stalkToFiber P x
      (Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ U.obj) }
        { val := f, property := h }) =
    f { val := x, property := (_ : x ∈ U.obj) }
[PROOFSTEP]
exact stalkToFiber_germ _ U.1 ⟨x, U.2⟩ ⟨f, h⟩
[GOAL]
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
⊢ tU = tV
[PROOFSTEP]
let Q :
  ∃ (W : (OpenNhds x)ᵒᵖ) (s : ∀ w : (unop W).1, T w) (hW : P.pred s),
    tU = (subsheafToTypes P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ ∧
      tV = (subsheafToTypes P).presheaf.germ ⟨x, (unop W).2⟩ ⟨s, hW⟩ :=
  ?_
[GOAL]
case refine_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
Q : ∃ W s hW,
  tU =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW } ∧
    tV =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW } :=
  ?refine_1
⊢ tU = tV
[PROOFSTEP]
choose W s hW e using Q
[GOAL]
case refine_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
W : (OpenNhds x)ᵒᵖ
s : (w : { x_1 // x_1 ∈ W.unop.obj }) → T ↑w
hW : PrelocalPredicate.pred P.toPrelocalPredicate s
e :
  tU =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW } ∧
    tV =
      Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
        { val := s, property := hW }
⊢ tU = tV
[PROOFSTEP]
exact e.1.trans e.2.symm
[GOAL]
case refine_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
tU tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
h : stalkToFiber P x tU = stalkToFiber P x tV
⊢ ∃ W s hW,
    tU =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      tV =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective'.{v, v} tU
[GOAL]
case refine_1.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
tV : Presheaf.stalk (Sheaf.presheaf (subsheafToTypes P)) x
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
h :
  stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        U { val := fU, property := hU }) =
    stalkToFiber P x tV
⊢ ∃ W s hW,
    colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
            (Sheaf.presheaf (subsheafToTypes P)))
          U { val := fU, property := hU } =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      tV =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective'.{v, v} tV
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h :
  stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        U { val := fU, property := hU }) =
    stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        V { val := fV, property := hV })
⊢ ∃ W s hW,
    colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
            (Sheaf.presheaf (subsheafToTypes P)))
          U { val := fU, property := hU } =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
            (Sheaf.presheaf (subsheafToTypes P)))
          V { val := fV, property := hV } =
        Presheaf.germ (Sheaf.presheaf (subsheafToTypes P)) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
dsimp
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h :
  stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        U { val := fU, property := hU }) =
    stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (Sheaf.presheaf (subsheafToTypes P)))
        V { val := fV, property := hV })
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
simp only [stalkToFiber, Types.Colimit.ι_desc_apply'] at h
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : { x_1 // x_1 ∈ U.obj }) → T ↑y),
    PrelocalPredicate.pred P.toPrelocalPredicate fU →
      ∀ (fV : (y : { x_2 // x_2 ∈ V.obj }) → T ↑y),
        PrelocalPredicate.pred P.toPrelocalPredicate fV →
          fU { val := x, property := (_ : x ∈ U.obj) } = fV { val := x, property := (_ : x ∈ V.obj) } →
            ∃ W iU iV,
              ∀ (w : { x_4 // x_4 ∈ W.obj }),
                fU ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑U.obj) }) w) =
                  fV ((fun x_4 => { val := ↑x_4, property := (_ : ↑x_4 ∈ ↑V.obj) }) w)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
specialize w (unop U) (unop V) fU hU fV hV h
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
w :
  ∃ W iU iV,
    ∀ (w : { x_1 // x_1 ∈ W.obj }),
      fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
        fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
rcases w with
  ⟨W, iU, iV, w⟩
    -- and put it back together again in the correct order.
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ ∃ W s hW,
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW } ∧
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
        Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ W.unop.obj) }
          { val := s, property := hW }
[PROOFSTEP]
refine' ⟨op W, fun w => fU (iU w : (unop U).1), P.res _ _ hU, _⟩
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ (op W).unop.obj ⟶ U.unop.obj
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) } ∧
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) }
[PROOFSTEP]
rcases W with ⟨W, m⟩
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_1.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : Opens ↑X
m : x ∈ W
iU : { obj := W, property := m } ⟶ U.unop
iV : { obj := W, property := m } ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ { obj := W, property := m }.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ (op { obj := W, property := m }).unop.obj ⟶ U.unop.obj
[PROOFSTEP]
exact iU
[GOAL]
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine'_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj U).unop }) → T ↑x_1
hU : PrelocalPredicate.pred P.toPrelocalPredicate fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : { x_1 // x_1 ∈ ((OpenNhds.inclusion x).op.obj V).unop }) → T ↑x_1
hV : PrelocalPredicate.pred P.toPrelocalPredicate fV
h : fU { val := x, property := (_ : x ∈ U.unop.obj) } = fV { val := x, property := (_ : x ∈ V.unop.obj) }
W : OpenNhds x
iU : W ⟶ U.unop
iV : W ⟶ V.unop
w :
  ∀ (w : { x_1 // x_1 ∈ W.obj }),
    fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w) =
      fV ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑V.unop.obj) }) w)
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U { val := fU, property := hU } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) } ∧
    colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V { val := fV, property := hV } =
      Presheaf.germ (subpresheafToTypes P.toPrelocalPredicate) { val := x, property := (_ : x ∈ (op W).unop.obj) }
        { val := fun w => fU ((fun x_1 => { val := ↑x_1, property := (_ : ↑x_1 ∈ ↑U.unop.obj) }) w),
          property :=
            (_ :
              PrelocalPredicate.pred P.toPrelocalPredicate fun x_1 =>
                fU ((fun x_2 => { val := ↑x_2, property := (_ : ↑x_2 ∈ ↑U.unop.obj) }) x_1)) }
[PROOFSTEP]
exact ⟨colimit_sound iU.op (Subtype.eq rfl), colimit_sound iV.op (Subtype.eq (funext w).symm)⟩
[GOAL]
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
⊢ (subpresheafToTypes (continuousPrelocal X✝ T)).obj X ⟶ (presheafToTop X✝ T).obj X
[PROOFSTEP]
rintro ⟨f, c⟩
[GOAL]
case mk
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
f : (x : { x // x ∈ X.unop }) → (fun x => ↑T) ↑x
c : PrelocalPredicate.pred (continuousPrelocal X✝ T) f
⊢ (presheafToTop X✝ T).obj X
[PROOFSTEP]
exact ⟨f, c⟩
[GOAL]
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
⊢ (presheafToTop X✝ T).obj X ⟶ (subpresheafToTypes (continuousPrelocal X✝ T)).obj X
[PROOFSTEP]
rintro ⟨f, c⟩
[GOAL]
case mk
X✝ : TopCat
T✝ : ↑X✝ → Type v
T : TopCat
X : (Opens ↑X✝)ᵒᵖ
f : ↑((Opens.toTopCat X✝).op.obj X).unop → ↑T
c : Continuous f
⊢ (subpresheafToTypes (continuousPrelocal X✝ T)).obj X
[PROOFSTEP]
exact ⟨f, c⟩


[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'))