case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X f

case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) = basicOpen X f
apply le_antisymm
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ V.unop ⊓ basicOpen X f ≤ basicOpen X f
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X f
rw [X.basicOpen_res i f]
no goals
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ V.unop ⊓ basicOpen X f ≤ basicOpen X f
exact inf_le_right
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(X.presheaf.map i ≫ X.presheaf.map (inv i)) f) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
have : X.basicOpen ((X.presheaf.map _ ≫ X.presheaf.map _) f) = _ :=
  X.basicOpen_res (inv i) (X.presheaf.map i f)
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(𝟙 (X.presheaf.obj U)) f) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(X.presheaf.map i ≫ X.presheaf.map (inv i)) f) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
rw [← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id] at this
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(𝟙 (X.presheaf.obj U)) f) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X (↑(X.presheaf.map i) f)
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(𝟙 (X.presheaf.obj U)) f) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ basicOpen X f ≤ basicOpen X (↑(X.presheaf.map i) f)
erw [this]
no goals
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
this : basicOpen X (↑(𝟙 (X.presheaf.obj U)) f) = U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f)
⊢ U.unop ⊓ basicOpen X (↑(X.presheaf.map i) f) ≤ basicOpen X (↑(X.presheaf.map i) f)
exact inf_le_right