[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ @UniversallyClosed = universally (topologically @IsClosedMap)
[PROOFSTEP]
ext X Y f
[GOAL]
case h.h.h.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyClosed f ↔ universally (topologically @IsClosedMap) f
[PROOFSTEP]
rw [UniversallyClosed_iff]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderComposition @UniversallyClosed
[PROOFSTEP]
rw [universallyClosed_eq]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderComposition (universally (topologically @IsClosedMap))
[PROOFSTEP]
exact StableUnderComposition.universally (fun X Y Z f g hf hg => @IsClosedMap.comp _ _ _ _ _ _ g.1.base f.1.base hg hf)
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ PropertyIsLocalAtTarget @UniversallyClosed
[PROOFSTEP]
rw [universallyClosed_eq]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ PropertyIsLocalAtTarget (universally (topologically @IsClosedMap))
[PROOFSTEP]
apply universallyIsLocalAtTargetOfMorphismRestrict
[GOAL]
case hP₁
X Y : Scheme
f : X ⟶ Y
⊢ RespectsIso (topologically @IsClosedMap)
[PROOFSTEP]
exact
  StableUnderComposition.respectsIso (fun X Y Z f g hf hg => @IsClosedMap.comp _ _ _ _ _ _ g.1.base f.1.base hg hf)
    (fun f => (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso f)).isClosedMap)
[GOAL]
case hP₂
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Opens ↑↑Y.toPresheafedSpace),
    iSup U = ⊤ → (∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)) → topologically (@IsClosedMap) f
[PROOFSTEP]
intro X Y f ι U hU H
[GOAL]
case hP₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑↑Y.toPresheafedSpace
hU : iSup U = ⊤
H : ∀ (i : ι), topologically (@IsClosedMap) (f ∣_ U i)
⊢ topologically (@IsClosedMap) f
[PROOFSTEP]
simp_rw [topologically, morphismRestrict_base] at H 
[GOAL]
case hP₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑↑Y.toPresheafedSpace
hU : iSup U = ⊤
H : ∀ (i : ι), IsClosedMap (Set.restrictPreimage (U i).carrier ↑f.val.base)
⊢ topologically (@IsClosedMap) f
[PROOFSTEP]
exact (isClosedMap_iff_isClosedMap_of_iSup_eq_top hU).mpr H
