[GOAL]
X Y : Scheme
f : X ⟶ Y
x✝ : QuasiCompact f
h : ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
⊢ Continuous ↑f.val.base
[PROOFSTEP]
continuity
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ QuasiCompact f
[PROOFSTEP]
constructor
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
intro U _ hU'
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
convert hU'.image (inv f.1.base).continuous_toFun using 1
[GOAL]
case h.e'_3.h
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ ↑f.val.base ⁻¹' U = (inv f.val.base).toFun '' U
[PROOFSTEP]
rw [Set.image_eq_preimage_of_inverse]
[GOAL]
case h.e'_3.h.h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ Function.LeftInverse (↑f.val.base) (inv f.val.base).toFun
case h.e'_3.h.h₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ Function.RightInverse (↑f.val.base) (inv f.val.base).toFun
[PROOFSTEP]
delta Function.LeftInverse
[GOAL]
case h.e'_3.h.h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ ∀ (x : ↑↑Y.toPresheafedSpace), ↑f.val.base (ContinuousMap.toFun (inv f.val.base) x) = x
case h.e'_3.h.h₂
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Set ↑↑Y.toPresheafedSpace
a✝ : IsOpen U
hU' : IsCompact U
e_1✝ : (forget TopCat).obj ↑X.toPresheafedSpace = ↑↑X.toPresheafedSpace
⊢ Function.RightInverse (↑f.val.base) (inv f.val.base).toFun
[PROOFSTEP]
exacts [IsIso.inv_hom_id_apply f.1.base, IsIso.hom_inv_id_apply f.1.base]
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
⊢ QuasiCompact (f ≫ g)
[PROOFSTEP]
constructor
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
⊢ ∀ (U : Set ↑↑Z.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑(f ≫ g).val.base ⁻¹' U)
[PROOFSTEP]
intro U hU hU'
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑(f ≫ g).val.base ⁻¹' U)
[PROOFSTEP]
rw [Scheme.comp_val_base, coe_comp, Set.preimage_comp]
[GOAL]
case isCompact_preimage
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑f.val.base ⁻¹' (↑g.val.base ⁻¹' U))
[PROOFSTEP]
apply QuasiCompact.isCompact_preimage
[GOAL]
case isCompact_preimage.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsOpen (↑g.val.base ⁻¹' U)
[PROOFSTEP]
exact
  Continuous.isOpen_preimage
    (by
      -- porting note: `continuity` failed
          -- see https://github.com/leanprover-community/mathlib4/issues/5030exact Scheme.Hom.continuous g)
    _ hU
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ Continuous ↑g.val.base
[PROOFSTEP]
exact Scheme.Hom.continuous g
[GOAL]
case isCompact_preimage.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑g.val.base ⁻¹' U)
[PROOFSTEP]
apply QuasiCompact.isCompact_preimage
[GOAL]
case isCompact_preimage.a.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsOpen U
[PROOFSTEP]
assumption
[GOAL]
case isCompact_preimage.a.a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↑↑Z.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact U
[PROOFSTEP]
assumption
[GOAL]
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ IsCompact U ∧ IsOpen U ↔ ∃ s, Set.Finite s ∧ U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion (fun (U : X.affineOpens) => (U : Opens X.carrier))
[GOAL]
case hb
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis (Set.range fun U => ↑U)
[PROOFSTEP]
rw [Subtype.range_coe]
[GOAL]
case hb
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ Opens.IsBasis (Scheme.affineOpens X)
[PROOFSTEP]
exact isBasis_affine_open X
[GOAL]
case hb'
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
U : Set ↑↑X.toPresheafedSpace
⊢ ∀ (i : ↑(Scheme.affineOpens X)), IsCompact ↑↑i
[PROOFSTEP]
exact fun i => i.2.isCompact
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
[PROOFSTEP]
rw [QuasiCompact_iff]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)) ↔
    ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
[PROOFSTEP]
refine' ⟨fun H U hU => H U U.isOpen hU.isCompact, _⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)) →
    ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
intro H U hU hU'
[GOAL]
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
U : Set ↑↑Y.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (↑f.val.base ⁻¹' U)
[PROOFSTEP]
obtain ⟨S, hS, rfl⟩ := (isCompact_open_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
S : Set ↑(Scheme.affineOpens Y)
hS : Set.Finite S
hU : IsOpen (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
hU' : IsCompact (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
⊢ IsCompact (↑f.val.base ⁻¹' ⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
[PROOFSTEP]
simp only [Set.preimage_iUnion]
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)
S : Set ↑(Scheme.affineOpens Y)
hS : Set.Finite S
hU : IsOpen (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
hU' : IsCompact (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑↑i)
⊢ IsCompact (⋃ (i : ↑(Scheme.affineOpens Y)) (_ : i ∈ S), ↑f.val.base ⁻¹' ↑↑i)
[PROOFSTEP]
exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.toProperty affineProperty f ↔ IsAffine Y ∧ CompactSpace ↑↑X.toPresheafedSpace
[PROOFSTEP]
delta AffineTargetMorphismProperty.toProperty QuasiCompact.affineProperty
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∃ h, CompactSpace ↑↑X.toPresheafedSpace) ↔ IsAffine Y ∧ CompactSpace ↑↑X.toPresheafedSpace
[PROOFSTEP]
simp
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ targetAffineLocally QuasiCompact.affineProperty f
[PROOFSTEP]
rw [quasiCompact_iff_forall_affine]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)) ↔
    targetAffineLocally QuasiCompact.affineProperty f
[PROOFSTEP]
trans ∀ U : Y.affineOpens, IsCompact (f.1.base ⁻¹' (U : Set Y.carrier))
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Opens ↑↑Y.toPresheafedSpace), IsAffineOpen U → IsCompact (↑f.val.base ⁻¹' ↑U)) ↔
    ∀ (U : ↑(Scheme.affineOpens Y)), IsCompact (↑f.val.base ⁻¹' ↑↑U)
[PROOFSTEP]
exact ⟨fun h U => h U U.prop, fun h U hU => h ⟨U, hU⟩⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : ↑(Scheme.affineOpens Y)), IsCompact (↑f.val.base ⁻¹' ↑↑U)) ↔ targetAffineLocally QuasiCompact.affineProperty f
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
X Y : Scheme
f : X ⟶ Y
⊢ ∀ (a : ↑(Scheme.affineOpens Y)), IsCompact (↑f.val.base ⁻¹' ↑↑a) ↔ QuasiCompact.affineProperty (f ∣_ ↑a)
[PROOFSTEP]
exact fun _ => isCompact_iff_compactSpace
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ @QuasiCompact = targetAffineLocally QuasiCompact.affineProperty
[PROOFSTEP]
ext
[GOAL]
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ QuasiCompact x✝ ↔ targetAffineLocally QuasiCompact.affineProperty x✝
[PROOFSTEP]
exact quasiCompact_iff_affineProperty _
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
⊢ IsCompact ↑(Scheme.basicOpen X f)
[PROOFSTEP]
classical
refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1
obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union _).mp ⟨hU, U.isOpen⟩
let g : s → X.affineOpens := by
  intro V
  use V.1 ⊓ X.basicOpen f
  have : V.1.1 ⟶ U := by
    apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e]
    convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
  erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
  exact IsAffineOpen.basicOpenIsAffine V.1.prop _
haveI : Finite s := hs.to_subtype
refine' ⟨Set.range g, Set.finite_range g, _⟩
refine' (Set.inter_eq_right_iff_subset.mpr (SetLike.coe_subset_coe.2 <| RingedSpace.basicOpen_le _ _)).symm.trans _
rw [e, Set.iUnion₂_inter]
apply le_antisymm <;> apply Set.iUnion₂_subset
· intro i hi
  exact
    Set.Subset.trans (Set.Subset.rfl : _ ≤ g ⟨i, hi⟩)
      (@Set.subset_iUnion₂ _ _ _ (fun (i : Scheme.affineOpens X) (_ : i ∈ Set.range g) => (i : Set X.toPresheafedSpace))
        _ (Set.mem_range_self ⟨i, hi⟩))
· rintro ⟨i, hi⟩ ⟨⟨j, hj⟩, hj'⟩
  rw [← hj']
  refine' Set.Subset.trans _ (Set.subset_iUnion₂ j hj)
  exact Set.Subset.rfl
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
⊢ IsCompact ↑(Scheme.basicOpen X f)
[PROOFSTEP]
refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union _).mp ⟨hU, U.isOpen⟩
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
let g : s → X.affineOpens := by
  intro V
  use V.1 ⊓ X.basicOpen f
  have : V.1.1 ⟶ U := by
    apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e]
    convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
  erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
  exact IsAffineOpen.basicOpenIsAffine V.1.prop _
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ↑s → ↑(Scheme.affineOpens X)
[PROOFSTEP]
intro V
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑(Scheme.affineOpens X)
[PROOFSTEP]
use V.1 ⊓ X.basicOpen f
[GOAL]
case property
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X
[PROOFSTEP]
have : V.1.1 ⟶ U := by
  apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e]
  convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑V ⟶ U
[PROOFSTEP]
apply homOfLE
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑V ≤ U
[PROOFSTEP]
change _ ⊆ (U : Set X.carrier)
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑↑V ⊆ ↑U
[PROOFSTEP]
rw [e]
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
⊢ ↑↑↑V ⊆ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
convert @Set.subset_iUnion₂ _ _ _ (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1
[GOAL]
case property
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
this : ↑↑V ⟶ U
⊢ ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X
[PROOFSTEP]
erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
[GOAL]
case property
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
V : ↑s
this : ↑↑V ⟶ U
⊢ RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace)
      (↑((LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace).toPresheafedSpace.presheaf.map this.op) f) ∈
    Scheme.affineOpens X
[PROOFSTEP]
exact IsAffineOpen.basicOpenIsAffine V.1.prop _
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
haveI : Finite s := hs.to_subtype
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ∃ s, Set.Finite s ∧ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
refine' ⟨Set.range g, Set.finite_range g, _⟩
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ↑(Scheme.basicOpen X f) = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
refine' (Set.inter_eq_right_iff_subset.mpr (SetLike.coe_subset_coe.2 <| RingedSpace.basicOpen_le _ _)).symm.trans _
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ↑U ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) =
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
rw [e, Set.iUnion₂_inter]
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) =
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
apply le_antisymm
[GOAL]
case intro.intro.a
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) ≤
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
apply Set.iUnion₂_subset
[GOAL]
case intro.intro.a
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i ≤
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
apply Set.iUnion₂_subset
[GOAL]
case intro.intro.a.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ∀ (i : ↑(Scheme.affineOpens X)),
    i ∈ s →
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) ⊆
        ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
intro i hi
[GOAL]
case intro.intro.a.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : ↑(Scheme.affineOpens X)
hi : i ∈ s
⊢ ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f) ⊆
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ Set.range g), ↑↑i
[PROOFSTEP]
exact
  Set.Subset.trans (Set.Subset.rfl : _ ≤ g ⟨i, hi⟩)
    (@Set.subset_iUnion₂ _ _ _ (fun (i : Scheme.affineOpens X) (_ : i ∈ Set.range g) => (i : Set X.toPresheafedSpace)) _
      (Set.mem_range_self ⟨i, hi⟩))
[GOAL]
case intro.intro.a.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
⊢ ∀ (i : ↑(Scheme.affineOpens X)),
    i ∈ Set.range g →
      ↑↑i ⊆
        ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
          ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
rintro ⟨i, hi⟩ ⟨⟨j, hj⟩, hj'⟩
[GOAL]
case intro.intro.a.h.mk.intro.mk
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : Opens ↑↑X.toPresheafedSpace
hi : i ∈ Scheme.affineOpens X
j : ↑(Scheme.affineOpens X)
hj : j ∈ s
hj' : g { val := j, property := hj } = { val := i, property := hi }
⊢ ↑↑{ val := i, property := hi } ⊆
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
rw [← hj']
[GOAL]
case intro.intro.a.h.mk.intro.mk
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : Opens ↑↑X.toPresheafedSpace
hi : i ∈ Scheme.affineOpens X
j : ↑(Scheme.affineOpens X)
hj : j ∈ s
hj' : g { val := j, property := hj } = { val := i, property := hi }
⊢ ↑↑(g { val := j, property := hj }) ⊆
    ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s),
      ↑↑i ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
refine' Set.Subset.trans _ (Set.subset_iUnion₂ j hj)
[GOAL]
case intro.intro.a.h.mk.intro.mk
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact ↑U
f : ↑(X.presheaf.obj (op U))
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : ↑U = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
g : ↑s → ↑(Scheme.affineOpens X) :=
  fun V => { val := ↑↑V ⊓ Scheme.basicOpen X f, property := (_ : ↑↑V ⊓ Scheme.basicOpen X f ∈ Scheme.affineOpens X) }
this : Finite ↑s
i : Opens ↑↑X.toPresheafedSpace
hi : i ∈ Scheme.affineOpens X
j : ↑(Scheme.affineOpens X)
hj : j ∈ s
hj' : g { val := j, property := hj } = { val := i, property := hi }
⊢ ↑↑(g { val := j, property := hj }) ⊆
    ↑↑j ∩ ↑(RingedSpace.basicOpen (LocallyRingedSpace.toRingedSpace X.toLocallyRingedSpace) f)
[PROOFSTEP]
exact Set.Subset.rfl
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.IsLocal affineProperty
[PROOFSTEP]
constructor
[GOAL]
case RespectsIso
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.RespectsIso (AffineTargetMorphismProperty.toProperty affineProperty)
[PROOFSTEP]
apply AffineTargetMorphismProperty.respectsIso_mk
[GOAL]
case RespectsIso.h₁
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z], affineProperty f → affineProperty (e.hom ≫ f)
[PROOFSTEP]
rintro X Y Z e _ _ H
[GOAL]
case RespectsIso.h₂
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [h : IsAffine Y], affineProperty f → affineProperty (f ≫ e.hom)
[PROOFSTEP]
rintro X Y Z e _ _ H
[GOAL]
case RespectsIso.h₁
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
e : X ≅ Y
f✝ : Y ⟶ Z
inst✝ : IsAffine Z
H : affineProperty f✝
⊢ affineProperty (e.hom ≫ f✝)
case RespectsIso.h₂
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
X Y Z : Scheme
e : Y ≅ Z
f✝ : X ⟶ Y
h✝ : IsAffine Y
H : affineProperty f✝
⊢ affineProperty (f✝ ≫ e.hom)
[PROOFSTEP]
exacts [@Homeomorph.compactSpace _ _ _ _ H (TopCat.homeoOfIso (asIso e.inv.1.base)), H]
[GOAL]
case toBasicOpen
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (op ⊤))),
    affineProperty f → affineProperty (f ∣_ Scheme.basicOpen Y r)
[PROOFSTEP]
introv H
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : affineProperty f
⊢ affineProperty (f ∣_ Scheme.basicOpen Y r)
[PROOFSTEP]
dsimp [affineProperty] at H ⊢
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ CompactSpace ↑((Opens.toTopCat ↑X.toPresheafedSpace).obj ((Opens.map f.val.base).obj (Scheme.basicOpen Y r)))
[PROOFSTEP]
change CompactSpace ((Opens.map f.val.base).obj (Y.basicOpen r))
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ CompactSpace { x // x ∈ (Opens.map f.val.base).obj (Scheme.basicOpen Y r) }
[PROOFSTEP]
rw [Scheme.preimage_basicOpen f r]
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ CompactSpace { x // x ∈ Scheme.basicOpen X (↑(NatTrans.app f.val.c (op ⊤)) r) }
[PROOFSTEP]
erw [← isCompact_iff_compactSpace]
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : CompactSpace ↑↑X.toPresheafedSpace
⊢ IsCompact ↑(Scheme.basicOpen X (↑(NatTrans.app f.val.c (op ⊤)) r))
[PROOFSTEP]
rw [← isCompact_univ_iff] at H 
[GOAL]
case toBasicOpen
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : IsCompact Set.univ
⊢ IsCompact ↑(Scheme.basicOpen X (↑(NatTrans.app f.val.c (op ⊤)) r))
[PROOFSTEP]
apply isCompact_basicOpen
[GOAL]
case toBasicOpen.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑(Y.presheaf.obj (op ⊤))
H : IsCompact Set.univ
⊢ IsCompact ↑((Opens.map f.val.base).obj ⊤)
[PROOFSTEP]
exact H
[GOAL]
case ofBasicOpenCover
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (s : Finset ↑(Y.presheaf.obj (op ⊤))),
    Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)) → affineProperty f
[PROOFSTEP]
rintro X Y H f S hS hS'
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ affineProperty f
[PROOFSTEP]
rw [← IsAffineOpen.basicOpen_union_eq_self_iff] at hS 
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ affineProperty f
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
delta QuasiCompact.affineProperty
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ CompactSpace ↑↑X.toPresheafedSpace
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
rw [← isCompact_univ_iff]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact Set.univ
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
change IsCompact ((Opens.map f.val.base).obj ⊤).1
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact ((Opens.map f.val.base).obj ⊤).carrier
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
rw [← hS]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact ((Opens.map f.val.base).obj (⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f)).carrier
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
dsimp [Opens.map]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact (↑f.val.base ⁻¹' ↑(⨆ (f : { x // x ∈ S }), Scheme.basicOpen Y ↑f))
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion]
[GOAL]
case ofBasicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : ⨆ (f : ↑↑S), Scheme.basicOpen Y ↑f = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsCompact (⋃ (i : { x // x ∈ S }), ↑f.val.base ⁻¹' ↑(Scheme.basicOpen Y ↑i))
case ofBasicOpenCover.hU
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑(Y.presheaf.obj (op ⊤))
hS : Ideal.span ↑S = ⊤
hS' : ∀ (r : { x // x ∈ S }), affineProperty (f ∣_ Scheme.basicOpen Y ↑r)
⊢ IsAffineOpen ⊤
[PROOFSTEP]
exacts [isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i), topIsAffineOpen _]
[GOAL]
X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.StableUnderBaseChange affineProperty
[PROOFSTEP]
intro X Y S _ _ f g h
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : affineProperty g
⊢ affineProperty pullback.fst
[PROOFSTEP]
rw [QuasiCompact.affineProperty] at h ⊢
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
skip
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
let 𝒰 := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
have : Finite 𝒰.J := by dsimp; infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
⊢ Finite 𝒰.J
[PROOFSTEP]
dsimp
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
⊢ Finite (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)).J
[PROOFSTEP]
infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
have : ∀ i, CompactSpace (𝒰.obj i).carrier := by intro i; dsimp; infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
⊢ ∀ (i : 𝒰.J), CompactSpace ↑↑(Scheme.OpenCover.obj 𝒰 i).toPresheafedSpace
[PROOFSTEP]
intro i
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
i : 𝒰.J
⊢ CompactSpace ↑↑(Scheme.OpenCover.obj 𝒰 i).toPresheafedSpace
[PROOFSTEP]
dsimp
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this : Finite 𝒰.J
i : 𝒰.J
⊢ CompactSpace
    ↑↑(pullback f
                (Scheme.OpenCover.map (Scheme.affineCover Y) (Scheme.OpenCover.f (Scheme.affineCover Y) ↑i) ≫
                  g)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
infer_instance
[GOAL]
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↑↑Y.toPresheafedSpace
𝒰 : Scheme.OpenCover (pullback f g) :=
  Scheme.Pullback.openCoverOfRight (Scheme.OpenCover.finiteSubcover (Scheme.affineCover Y)) f g
this✝ : Finite 𝒰.J
this : ∀ (i : 𝒰.J), CompactSpace ↑↑(Scheme.OpenCover.obj 𝒰 i).toPresheafedSpace
⊢ CompactSpace ↑↑(pullback f g).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
[PROOFSTEP]
exact 𝒰.compactSpace
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
⊢ P S
[PROOFSTEP]
classical
obtain ⟨s, hs, hs'⟩ := (isCompact_open_iff_eq_finset_affine_union S.1).mp ⟨hS, S.2⟩
replace hs' : S = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs'
subst hs'
apply @Set.Finite.induction_on _ _ _ hs
· convert h₁; rw [iSup_eq_bot]; rintro ⟨_, h⟩; exact h.elim
· intro x s _ hs h₄
  have : IsCompact (⨆ i : s, (i : Opens X.carrier)).1 := by
    refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1; exact ⟨s, hs, by simp⟩
  convert h₂ _ this x h₄
  rw [iSup_subtype, sup_comm]
  conv_rhs => rw [iSup_subtype]
  exact iSup_insert
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
⊢ P S
[PROOFSTEP]
obtain ⟨s, hs, hs'⟩ := (isCompact_open_iff_eq_finset_affine_union S.1).mp ⟨hS, S.2⟩
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ P S
[PROOFSTEP]
replace hs' : S = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs'
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ S = ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
ext1
[GOAL]
case h
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ↑S = ↑(⨆ (i : ↑s), ↑↑i)
[PROOFSTEP]
simpa using hs'
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
S : Opens ↑↑X.toPresheafedSpace
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hs' : S = ⨆ (i : ↑s), ↑↑i
⊢ P S
[PROOFSTEP]
subst hs'
[GOAL]
case intro.intro
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ P (⨆ (i : ↑s), ↑↑i)
[PROOFSTEP]
apply @Set.Finite.induction_on _ _ _ hs
[GOAL]
case intro.intro.H0
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ P (⨆ (i : ↑∅), ↑↑i)
[PROOFSTEP]
convert h₁
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑∅), ↑↑i = ⊥
[PROOFSTEP]
rw [iSup_eq_bot]
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ∀ (i : ↑∅), ↑↑i = ⊥
[PROOFSTEP]
rintro ⟨_, h⟩
[GOAL]
case h.e'_1.mk
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
val✝ : ↑(Scheme.affineOpens X)
h : val✝ ∈ ∅
⊢ ↑↑{ val := val✝, property := h } = ⊥
[PROOFSTEP]
exact h.elim
[GOAL]
case intro.intro.H1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
hS : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ∀ {a : ↑(Scheme.affineOpens X)} {s : Set ↑(Scheme.affineOpens X)},
    ¬a ∈ s → Set.Finite s → P (⨆ (i : ↑s), ↑↑i) → P (⨆ (i : ↑(insert a s)), ↑↑i)
[PROOFSTEP]
intro x s _ hs h₄
[GOAL]
case intro.intro.H1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ P (⨆ (i : ↑(insert x s)), ↑↑i)
[PROOFSTEP]
have : IsCompact (⨆ i : s, (i : Opens X.carrier)).1 := by
  refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1; exact ⟨s, hs, by simp⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ IsCompact (⨆ (i : ↑s), ↑↑i).carrier
[PROOFSTEP]
refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ ∃ s_1, Set.Finite s_1 ∧ (⨆ (i : ↑s), ↑↑i).carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s_1), ↑↑i
[PROOFSTEP]
exact ⟨s, hs, by simp⟩
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
⊢ (⨆ (i : ↑s), ↑↑i).carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
[PROOFSTEP]
simp
[GOAL]
case intro.intro.H1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ P (⨆ (i : ↑(insert x s)), ↑↑i)
[PROOFSTEP]
convert h₂ _ this x h₄
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑(insert x s)), ↑↑i = (⨆ (i : ↑s), ↑↑i) ⊔ ↑x
[PROOFSTEP]
rw [iSup_subtype, sup_comm]
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑(Scheme.affineOpens X)) (h : i ∈ insert x s), ↑↑{ val := i, property := h } = ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
conv_rhs => rw [iSup_subtype]
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
| ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
rw [iSup_subtype]
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
| ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
rw [iSup_subtype]
[GOAL]
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
| ↑x ⊔ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
rw [iSup_subtype]
[GOAL]
case h.e'_1
X Y : Scheme
f : X ⟶ Y
Z : Scheme
P : Opens ↑↑X.toPresheafedSpace → Prop
h₁ : P ⊥
h₂ : ∀ (S : Opens ↑↑X.toPresheafedSpace), IsCompact S.carrier → ∀ (U : ↑(Scheme.affineOpens X)), P S → P (S ⊔ ↑U)
s✝ : Set ↑(Scheme.affineOpens X)
hs✝ : Set.Finite s✝
hS : IsCompact (⨆ (i : ↑s✝), ↑↑i).carrier
x : ↑(Scheme.affineOpens X)
s : Set ↑(Scheme.affineOpens X)
a✝ : ¬x ∈ s
hs : Set.Finite s
h₄ : P (⨆ (i : ↑s), ↑↑i)
this : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
⊢ ⨆ (i : ↑(Scheme.affineOpens X)) (h : i ∈ insert x s), ↑↑{ val := i, property := h } =
    ↑x ⊔ ⨆ (i : ↑(Scheme.affineOpens X)) (h : i ∈ s), ↑↑{ val := i, property := h }
[PROOFSTEP]
exact iSup_insert
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op)] at H 
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = ↑(X.presheaf.map (homOfLE (_ : Scheme.basicOpen X f ≤ U)).op) 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
obtain ⟨⟨_, n, rfl⟩, e⟩ := (isLocalization_basicOpen hU f).eq_iff_exists'.mp H
[GOAL]
case intro.mk.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = ↑(X.presheaf.map (homOfLE (_ : Scheme.basicOpen X f ≤ U)).op) 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
exact ⟨n, by simpa [mul_comm x] using e⟩
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z : Scheme
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsAffineOpen U
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = ↑(X.presheaf.map (homOfLE (_ : Scheme.basicOpen X f ≤ U)).op) 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      x =
    ↑{ val := (fun x x_1 => x ^ x_1) f n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) f y = (fun x x_1 => x ^ x_1) f n) } *
      0
⊢ f ^ n * x = 0
[PROOFSTEP]
simpa [mul_comm x] using e
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union U.1).mp ⟨hU, U.2⟩
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
replace e : U = iSup fun i : s => (i : Opens X.carrier)
[GOAL]
case e
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ U = ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
ext1
[GOAL]
case e.h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U.carrier = ⋃ (i : ↑(Scheme.affineOpens X)) (_ : i ∈ s), ↑↑i
⊢ ↑U = ↑(⨆ (i : ↑s), ↑↑i)
[PROOFSTEP]
simpa using e
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
have h₁ : ∀ i : s, i.1.1 ≤ U := by
  intro i
  change (i : Opens X.carrier) ≤ U
  rw [e]
    -- porting note: `exact le_iSup _ _` no longer works
  exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
⊢ ∀ (i : ↑s), ↑↑i ≤ U
[PROOFSTEP]
intro i
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
i : ↑s
⊢ ↑↑i ≤ U
[PROOFSTEP]
change (i : Opens X.carrier) ≤ U
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
i : ↑s
⊢ ↑↑i ≤ U
[PROOFSTEP]
rw [e]
  -- porting note: `exact le_iSup _ _` no longer works
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
i : ↑s
⊢ ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
[PROOFSTEP]
exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _
[GOAL]
case intro.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
have H' := fun i : s =>
  exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen X i.1.2 (X.presheaf.map (homOfLE (h₁ i)).op x)
    (X.presheaf.map (homOfLE (h₁ i)).op f) ?_
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n, ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
⊢ ∃ n, f ^ n * x = 0
case intro.intro.refine_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x |_
      Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f) =
    0
[PROOFSTEP]
swap
[GOAL]
case intro.intro.refine_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x |_
      Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f) =
    0
[PROOFSTEP]
delta TopCat.Presheaf.restrictOpen TopCat.Presheaf.restrict at H ⊢
[GOAL]
case intro.intro.refine_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map
          (homOfLE
              (_ :
                ∀ ⦃a : ↑↑X.toPresheafedSpace⦄,
                  a ∈ ↑(Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f)) → a ∈ ↑↑↑i)).op)
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    0
[PROOFSTEP]
convert congr_arg (X.presheaf.map (homOfLE _).op) H
[GOAL]
case h.e'_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map
          (homOfLE
              (_ :
                ∀ ⦃a : ↑↑X.toPresheafedSpace⦄,
                  a ∈ ↑(Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f)) → a ∈ ↑↑↑i)).op)
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    ↑(X.presheaf.map (homOfLE ?intro.intro.refine_1.convert_1).op)
      (↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x)
[PROOFSTEP]
simp only [← comp_apply, ← Functor.map_comp]
[GOAL]
case h.e'_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ↑(X.presheaf.map
          ((homOfLE (_ : ↑↑i ≤ U)).op ≫
            (homOfLE
                (_ :
                  ∀ ⦃a : ↑↑X.toPresheafedSpace⦄,
                    a ∈ ↑(Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f)) → a ∈ ↑↑↑i)).op))
      x =
    ↑(X.presheaf.map
          ((homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op ≫
            (homOfLE ?intro.intro.refine_1.convert_1).op))
      x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ 0 = ↑(X.presheaf.map (homOfLE ?intro.intro.refine_1.convert_1).op) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case intro.intro.refine_1.convert_1
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : ↑(X.presheaf.map (homOfLE (_ : ∀ ⦃a : ↑↑X.toPresheafedSpace⦄, a ∈ ↑(Scheme.basicOpen X f) → a ∈ ↑U)).op) x = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ Scheme.basicOpen X (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f) ≤ Scheme.basicOpen X f
[PROOFSTEP]
simp only [Scheme.basicOpen_res, ge_iff_le, inf_le_right]
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n, ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
choose n hn using H'
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
case intro.intro.refine_2
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro.intro.refine_2.intro
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ n, f ^ n * x = 0
[PROOFSTEP]
use Finset.univ.sup n
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ f ^ Finset.sup Finset.univ n * x = 0
[PROOFSTEP]
suffices ∀ i : s, X.presheaf.map (homOfLE (h₁ i)).op (f ^ Finset.univ.sup n * x) = 0
  by
  subst e
  apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : Opens X.carrier)
  intro i
  rw [map_zero]
  apply this
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this✝ : Finite ↑s
val✝ : Fintype ↑s
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
⊢ f ^ Finset.sup Finset.univ n * x = 0
[PROOFSTEP]
subst e
[GOAL]
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
⊢ f ^ Finset.sup Finset.univ n * x = 0
[PROOFSTEP]
apply TopCat.Sheaf.eq_of_locally_eq X.sheaf fun i : s => (i : Opens X.carrier)
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
⊢ ∀ (i : ↑s),
    ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) (f ^ Finset.sup Finset.univ n * x) =
      ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) 0
[PROOFSTEP]
intro i
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
i : ↑s
⊢ ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) (f ^ Finset.sup Finset.univ n * x) =
    ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
n : ↑s → ℕ
this✝ : Finite ↑s
val✝ : Fintype ↑s
hU : IsCompact (⨆ (i : ↑s), ↑↑i).carrier
x f : ↑(X.presheaf.obj (op (⨆ (i : ↑s), ↑↑i)))
H : x |_ Scheme.basicOpen X f = 0
h₁ : ∀ (i : ↑s), ↑↑i ≤ ⨆ (i : ↑s), ↑↑i
hn :
  ∀ (i : ↑s),
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) f ^ n i *
        ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) x =
      0
this : ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ ⨆ (i : ↑s), ↑↑i)).op) (f ^ Finset.sup Finset.univ n * x) = 0
i : ↑s
⊢ ↑((Scheme.sheaf X).val.map (Opens.leSupr (fun i => ↑↑i) i).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
apply this
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
intro i
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s), ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x = 0
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
replace hn := congr_arg (fun x => X.presheaf.map (homOfLE (h₁ i)).op (f ^ (Finset.univ.sup n - n i)) * x) (hn i)
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  (fun x => ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * x)
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    (fun x => ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * x) 0
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
dsimp at hn 
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) *
      (↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) f ^ n i * ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) x) =
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * 0
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
simp only [← map_mul, ← map_pow] at hn 
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i) * (f ^ n i * x)) =
    ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i)) * 0
⊢ ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ Finset.sup Finset.univ n * x) = 0
[PROOFSTEP]
rwa [mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn 
[GOAL]
case h
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
Z X : Scheme
U : Opens ↑↑X.toPresheafedSpace
hU : IsCompact U.carrier
x f : ↑(X.presheaf.obj (op U))
H : x |_ Scheme.basicOpen X f = 0
s : Set ↑(Scheme.affineOpens X)
hs : Set.Finite s
e : U = ⨆ (i : ↑s), ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn : ↑(X.presheaf.map (homOfLE (_ : ↑↑i ≤ U)).op) (f ^ (Finset.sup Finset.univ n - n i + n i) * x) = 0
⊢ n i ≤ Finset.sup Finset.univ n
[PROOFSTEP]
apply Finset.le_sup (Finset.mem_univ i)
