[GOAL]
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
⊢ Function.Injective fun g => comp (sigmaMk g.fst) g.snd
[PROOFSTEP]
rintro ⟨i, g⟩ ⟨i', g'⟩ h
[GOAL]
case mk.mk
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g : C(X, Y i)
i' : ι
g' : C(X, Y i')
h :
  (fun g => comp (sigmaMk g.fst) g.snd) { fst := i, snd := g } =
    (fun g => comp (sigmaMk g.fst) g.snd) { fst := i', snd := g' }
⊢ { fst := i, snd := g } = { fst := i', snd := g' }
[PROOFSTEP]
obtain ⟨rfl, hg⟩ : i = i' ∧ HEq (⇑g) (⇑g') := Function.eq_of_sigmaMk_comp <| congr_arg FunLike.coe h
[GOAL]
case mk.mk.intro
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : (i : ι) → TopologicalSpace (Y i)
inst✝ : Nonempty X
i : ι
g g' : C(X, Y i)
h :
  (fun g => comp (sigmaMk g.fst) g.snd) { fst := i, snd := g } =
    (fun g => comp (sigmaMk g.fst) g.snd) { fst := i, snd := g' }
hg : HEq ↑g ↑g'
⊢ { fst := i, snd := g } = { fst := i, snd := g' }
[PROOFSTEP]
simpa using hg


[GOAL]
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) = U
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) ≤ U
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ ∀ (i : (V : Opens ↑X) × { f // R f }), coveringOfPresieve U R i ≤ U
[PROOFSTEP]
intro f
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
f : (V : Opens ↑X) × { f // R f }
⊢ coveringOfPresieve U R f ≤ U
[PROOFSTEP]
exact f.2.1.le
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ U ≤ iSup (coveringOfPresieve U R)
[PROOFSTEP]
intro x hxU
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup (coveringOfPresieve U R))
[PROOFSTEP]
rw [Opens.coe_iSup, Set.mem_iUnion]
[GOAL]
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)
[PROOFSTEP]
obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU
[GOAL]
case a.intro.intro.intro.intro.intro.intro.intro
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
V : Opens ↑X
iVU : V ⟶ U
hxV : x ∈ V
W : Opens ↑X
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)
[PROOFSTEP]
exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩
[GOAL]
X : TopCat
Y : Opens ↑X
R : Presieve Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
[PROOFSTEP]
funext Z
[GOAL]
case h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R
[PROOFSTEP]
ext f
[GOAL]
case h.h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
⊢ f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y ↔ f ∈ R
[PROOFSTEP]
exact ⟨fun ⟨⟨_, f', h⟩, rfl⟩ => by rwa [Subsingleton.elim f f'], fun h => ⟨⟨Z, f, h⟩, rfl⟩⟩
[GOAL]
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
x✝ : f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y
f' : Z ⟶ Y
h : R f'
⊢ f ∈ R
[PROOFSTEP]
rwa [Subsingleton.elim f f']
[GOAL]
X : TopCat
ι : Type v
U : ι → Opens ↑X
⊢ Sieve.generate (presieveOfCovering U) ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) (iSup U)
[PROOFSTEP]
intro x hx
[GOAL]
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨i, hxi⟩ := Opens.mem_iSup.mp hx
[GOAL]
case intro
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
[PROOFSTEP]
exact ⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩
[GOAL]
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B ↔ Opens.IsBasis (Set.range B.obj)
[PROOFSTEP]
rw [Opens.isBasis_iff_nbhd]
[GOAL]
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B ↔
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
[PROOFSTEP]
constructor
[GOAL]
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ CoverDense (Opens.grothendieckTopology ↑X) B →
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
intro hd U x hx
[GOAL]
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
rcases hd.1 U x hx with ⟨V, f, ⟨i, f₁, f₂, _⟩, hV⟩
[GOAL]
case mp.intro.intro.intro.intro.mk
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hd : CoverDense (Opens.grothendieckTopology ↑X) B
U : Opens ↑X
x : ↑X
hx : x ∈ U
V : Opens ↑X
f : V ⟶ U
hV : x ∈ V
i : ι
f₁ : V ⟶ B.obj i
f₂ : B.obj i ⟶ U
fac✝ : f₁ ≫ f₂ = f
⊢ ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
exact ⟨B.obj i, ⟨i, rfl⟩, f₁.le hV, f₂.le⟩
[GOAL]
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
⊢ (∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U) →
    CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
intro hb
[GOAL]
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ CoverDense (Opens.grothendieckTopology ↑X) B
[PROOFSTEP]
constructor
[GOAL]
case mpr.is_cover
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
[PROOFSTEP]
intro U x hx
[GOAL]
case mpr.is_cover
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
[PROOFSTEP]
rcases hb hx with ⟨_, ⟨i, rfl⟩, hx, hi⟩
[GOAL]
case mpr.is_cover.intro.intro.intro.intro
X : TopCat
ι : Type u_1
inst✝ : Category.{u_2, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U', U' ∈ Set.range B.obj ∧ x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx✝ : x ∈ U
i : ι
hx : x ∈ B.obj i
hi : B.obj i ≤ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
[PROOFSTEP]
exact ⟨B.obj i, ⟨⟨hi⟩⟩, ⟨⟨i, 𝟙 _, ⟨⟨hi⟩⟩, rfl⟩⟩, hx⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ↑f))
[PROOFSTEP]
haveI : Mono f := (TopCat.mono_iff_injective f).mpr hf.inj
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) (IsOpenMap.functor (_ : IsOpenMap ↑f))
[PROOFSTEP]
apply compatiblePreservingOfDownwardsClosed
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
⊢ {c : Opens ↑X} →
    {d : Opens ↑Y} →
      (d ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj c) →
        (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj c' ≅ d)
[PROOFSTEP]
intro U V i
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj U
⊢ (c' : Opens ↑X) × ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj c' ≅ V)
[PROOFSTEP]
refine' ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ _⟩
[GOAL]
case hF
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range fun x => ↑f x
[PROOFSTEP]
obtain ⟨_, _, rfl⟩ := i.le h
[GOAL]
case hF.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : OpenEmbedding ↑f
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj U
w✝ : (forget TopCat).obj X
left✝ : w✝ ∈ ↑U
h : ↑f w✝ ∈ V.1
⊢ ↑f w✝ ∈ Set.range fun x => ↑f x
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) (functor hf)
[PROOFSTEP]
constructor
[GOAL]
case cover_preserve
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
⊢ ∀ {U : Opens ↑X} {S : Sieve U},
    S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U →
      Sieve.functorPushforward (functor hf) S ∈
        GrothendieckTopology.sieves (Opens.grothendieckTopology ↑Y) ((functor hf).obj U)
[PROOFSTEP]
rintro U S hU _ ⟨x, hx, rfl⟩
[GOAL]
case cover_preserve.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ ↑f x ∈ U_1
[PROOFSTEP]
obtain ⟨V, i, hV, hxV⟩ := hU x hx
[GOAL]
case cover_preserve.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
hf : IsOpenMap ↑f
U : Opens ↑X
S : Sieve U
hU : S ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
x : (forget TopCat).obj X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (functor hf) S).arrows f_1 ∧ ↑f x ∈ U_1
[PROOFSTEP]
exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F✝ : Presheaf C X
F' : Sheaf C X
h✝ : Opens.IsBasis (Set.range B)
F : Sheaf C X
U : Opens ↑X
h : U = ⊥
⊢ Limits.IsTerminal (F.val.obj (op U))
[PROOFSTEP]
convert F.isTerminalOfEmpty
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val
i : ι
⊢ NatTrans.app (↑(restrictHomEquivHom F F' h) α) (op (B i)) = NatTrans.app α (op i)
[PROOFSTEP]
nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.val
i : ι
⊢ NatTrans.app (↑(restrictHomEquivHom F F' h) α) (op (B i)) =
    NatTrans.app (Equiv.invFun (restrictHomEquivHom F F' h) (Equiv.toFun (restrictHomEquivHom F F' h) α)) (op i)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), NatTrans.app α (op (B i)) = NatTrans.app β (op (B i))
⊢ α = β
[PROOFSTEP]
apply (restrictHomEquivHom F F' h).symm.injective
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), NatTrans.app α (op (B i)) = NatTrans.app β (op (B i))
⊢ ↑(restrictHomEquivHom F F' h).symm α = ↑(restrictHomEquivHom F F' h).symm β
[PROOFSTEP]
ext i
[GOAL]
case a.w.h
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.val
he : ∀ (i : ι), NatTrans.app α (op (B i)) = NatTrans.app β (op (B i))
i : (InducedCategory (Opens ↑X) B)ᵒᵖ
⊢ NatTrans.app (↑(restrictHomEquivHom F F' h).symm α) i = NatTrans.app (↑(restrictHomEquivHom F F' h).symm β) i
[PROOFSTEP]
exact he i.unop


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : CocompactMap α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : CocompactMap α β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
cocompact_tendsto'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (cocompact β)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ } =
    (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
cocompact_tendsto'✝¹ : Tendsto (ContinuousMap.mk toFun✝¹).toFun (cocompact α) (cocompact β)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
cocompact_tendsto'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (cocompact β)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝¹, cocompact_tendsto' := cocompact_tendsto'✝¹ } =
    (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, cocompact_tendsto' := cocompact_tendsto'✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Continuous f'
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Continuous ↑f
[PROOFSTEP]
exact f.continuous_toFun
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Tendsto (ContinuousMap.mk f').toFun (cocompact α) (cocompact β)
[PROOFSTEP]
simp_rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Tendsto (↑f) (cocompact α) (cocompact β)
[PROOFSTEP]
exact f.cocompact_tendsto'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
h : ∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)
s : Set β
hs : s ∈ cocompact β
t : Set β
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ (f ⁻¹' t)ᶜ ⊆ f ⁻¹' s
[PROOFSTEP]
simpa using preimage_mono hts
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
⊢ IsCompact (↑f ⁻¹' s)
[PROOFSTEP]
obtain ⟨t, ht, hts⟩ :=
  mem_cocompact'.mp
    (by
      simpa only [preimage_image_preimage, preimage_compl] using
        mem_map.mp
          (cocompact_tendsto f <| mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
⊢ ?m.10429 ∈ cocompact ?m.10404
[PROOFSTEP]
simpa only [preimage_image_preimage, preimage_compl] using
  mem_map.mp (cocompact_tendsto f <| mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
t : Set α
ht : IsCompact t
hts : (↑f ⁻¹' s)ᶜᶜ ⊆ t
⊢ IsCompact (↑f ⁻¹' s)
[PROOFSTEP]
exact isCompact_of_isClosed_subset ht (hs.isClosed.preimage <| map_continuous f) (by simpa using hts)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
t : Set α
ht : IsCompact t
hts : (↑f ⁻¹' s)ᶜᶜ ⊆ t
⊢ ↑f ⁻¹' s ⊆ t
[PROOFSTEP]
simpa using hts
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ Tendsto (ContinuousMap.mk ↑f).toFun (cocompact α) (cocompact β)
[PROOFSTEP]
refine' CocompactMap.tendsto_of_forall_preimage fun K hK => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ IsCompact ((ContinuousMap.mk ↑f).toFun ⁻¹' K)
[PROOFSTEP]
erw [K.preimage_equiv_eq_image_symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ IsCompact (↑f.symm '' K)
[PROOFSTEP]
exact hK.image f.symm.continuous


[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ IsLocallySurjective T → ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
[PROOFSTEP]
intro hT
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
⊢ (∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)) → IsLocallySurjective T
[PROOFSTEP]
intro hT
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
⊢ ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
[PROOFSTEP]
intro x g
[GOAL]
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
g : (forget C).obj ((stalkFunctor C x).obj 𝒢)
⊢ ∃ a, ↑((stalkFunctor C x).map T) a = g
[PROOFSTEP]
obtain ⟨U, hxU, t, rfl⟩ := 𝒢.germ_exist x g
[GOAL]
case mp.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
⊢ ∃ a, ↑((stalkFunctor C x).map T) a = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
rcases hT U t x hxU with
  ⟨V, ι, ⟨s, h_eq⟩, hxV⟩
    -- Then the germ of s maps to g.
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
h_eq : ↑(NatTrans.app T (op V)) s = ↑(𝒢.map ι.op) t
⊢ ∃ a, ↑((stalkFunctor C x).map T) a = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
use ℱ.germ ⟨x, hxV⟩ s
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
h_eq : ↑(NatTrans.app T (op V)) s = ↑(𝒢.map ι.op) t
⊢ ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
convert stalkFunctor_map_germ_apply V ⟨x, hxV⟩ T s using 1
[GOAL]
case h.e'_3.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : IsLocallySurjective T
x : ↑X
U : Opens ↑X
hxU : x ∈ U
t : (forget C).obj (𝒢.obj (op U))
V : Opens ↑X
ι : V ⟶ U
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
h_eq : ↑(NatTrans.app T (op V)) s = ↑(𝒢.map ι.op) t
e_1✝ :
  (forget C).obj ((stalkFunctor C x).obj 𝒢) =
    (forget C).obj (Limits.colim.obj ((OpenNhds.inclusion ↑{ val := x, property := hxV }).op ⋙ 𝒢))
⊢ ↑(germ 𝒢 { val := x, property := hxU }) t =
    ↑(Limits.colimit.ι ((OpenNhds.inclusion ↑{ val := x, property := hxV }).op ⋙ 𝒢)
          (op { obj := V, property := (_ : ↑{ val := x, property := hxV } ∈ V) }))
      (↑(NatTrans.app T (op V)) s)
[PROOFSTEP]
simpa [h_eq] using (germ_res_apply 𝒢 ι ⟨x, hxV⟩ t).symm
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
⊢ IsLocallySurjective T
[PROOFSTEP]
intro U t x hxU
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
set t_x := 𝒢.germ ⟨x, hxU⟩ t with ht_x
[GOAL]
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
[GOAL]
case mpr.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
s_x : (forget C).obj ((stalkFunctor C x).obj ℱ)
hs_x : ↑((stalkFunctor C x).map T) s_x = t_x
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨V, hxV, s, rfl⟩ := ℱ.germ_exist x s_x
[GOAL]
case mpr.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
have key_W :=
  𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
    convert hs_x using 1
    symm
    convert stalkFunctor_map_germ_apply _ _ _ s
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
⊢ ↑(germ 𝒢 { val := x, property := hxV }) (↑(NatTrans.app T (op V)) s) = ↑(germ 𝒢 { val := x, property := hxU }) t
[PROOFSTEP]
convert hs_x using 1
[GOAL]
case h.e'_2.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
e_1✝ :
  (fun x_1 => (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxV })) (↑(NatTrans.app T (op V)) s) =
    (fun x_1 => (forget C).obj ((stalkFunctor C x).obj 𝒢)) (↑(germ ℱ { val := x, property := hxV }) s)
⊢ ↑(germ 𝒢 { val := x, property := hxV }) (↑(NatTrans.app T (op V)) s) =
    ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s)
[PROOFSTEP]
symm
[GOAL]
case h.e'_2.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
e_1✝ :
  (fun x_1 => (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxV })) (↑(NatTrans.app T (op V)) s) =
    (fun x_1 => (forget C).obj ((stalkFunctor C x).obj 𝒢)) (↑(germ ℱ { val := x, property := hxV }) s)
⊢ ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) =
    ↑(germ 𝒢 { val := x, property := hxV }) (↑(NatTrans.app T (op V)) s)
[PROOFSTEP]
convert stalkFunctor_map_germ_apply _ _ _ s
[GOAL]
case mpr.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
key_W : ∃ W _m iU iV, ↑(𝒢.map iU.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map iV.op) t
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq : ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map hWU.op) t
⊢ ∃ U_1 f, (imageSieve T t).arrows f ∧ x ∈ U_1
[PROOFSTEP]
refine' ⟨W, hWU, ⟨ℱ.map hWV.op s, _⟩, hxW⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq : ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map hWU.op) t
⊢ ↑(NatTrans.app T (op W)) (↑(ℱ.map hWV.op) s) = ↑(𝒢.map hWU.op) t
[PROOFSTEP]
convert h_eq using 1
[GOAL]
case h.e'_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
X : TopCat
ℱ 𝒢 : Presheaf C X
inst✝¹ : Limits.HasColimits C
inst✝ : Limits.PreservesFilteredColimits (forget C)
T : ℱ ⟶ 𝒢
hT : ∀ (x : ↑X), Function.Surjective ↑((stalkFunctor C x).map T)
U : Opens ↑X
t : (forget C).obj (𝒢.obj (op U))
x : ↑X
hxU : x ∈ U
t_x : (forget C).obj (stalk 𝒢 ↑{ val := x, property := hxU }) := ↑(germ 𝒢 { val := x, property := hxU }) t
ht_x : t_x = ↑(germ 𝒢 { val := x, property := hxU }) t
V : Opens ↑X
hxV : x ∈ V
s : (forget C).obj (ℱ.obj (op V))
hs_x : ↑((stalkFunctor C x).map T) (↑(germ ℱ { val := x, property := hxV }) s) = t_x
W : Opens ↑X
hxW : x ∈ W
hWV : W ⟶ V
hWU : W ⟶ U
h_eq : ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s) = ↑(𝒢.map hWU.op) t
⊢ ↑(NatTrans.app T (op W)) (↑(ℱ.map hWV.op) s) = ↑(𝒢.map hWV.op) (↑(NatTrans.app T (op V)) s)
[PROOFSTEP]
simp only [← comp_apply, T.naturality]