-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme.{u})
    {U : X.Opens} (hU : IsCompact U.1) (x f : Γ(X, U))
    (H : x |_ (X.basicOpen f) = 0) :
    ∃ n : ℕ, f ^ n * x = 0

Proof state:
case intro.intro.refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n,
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
        0
⊢ ∃ n, f ^ n * x = 0

case intro.intro.refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x |_
        X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))
      ⋯ =
    0

Tactic:
swap

Result:
case intro.intro.refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x |_
        X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))
      ⋯ =
    0

case intro.intro.refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n,
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
        0
⊢ ∃ n, f ^ n * x = 0

Proof state:
case h.e'_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) x =
    (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ?intro.intro.refine_1.convert_1).op))) x

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
obtain ⟨s, hs, e⟩ := (isCompactOpen_iff_eq_finset_affine_union U.1).mp ⟨hU, U.2⟩

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, ↑↑i
⊢ ∃ n, f ^ n * x = 0

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
⊢ ∃ n, f ^ n * x = 0

Tactic:
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) ?_

Result:
case intro.intro.refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n,
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
        0
⊢ ∃ n, f ^ n * x = 0

case intro.intro.refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x |_
        X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))
      ⋯ =
    0

Proof state:
case h.e'_3
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ 0 = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ?intro.intro.refine_1.convert_1).op)) 0

Tactic:
rw [map_zero]

Result:
no goals

Proof state:
case intro.intro.refine_1.convert_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ≤ X.basicOpen f

Tactic:
simp only [Scheme.basicOpen_res, inf_le_right]

Result:
no goals

Proof state:
case intro.intro.refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n,
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
        0
⊢ ∃ n, f ^ n * x = 0

Tactic:
choose n hn using H'

Result:
case intro.intro.refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
⊢ ∃ n, f ^ n * x = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
i : ↑s
⊢ ↑↑i ≤ ⨆ i, ↑↑i

Tactic:
exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, ↑↑i
⊢ U = ⨆ i, ↑↑i

Tactic:
ext1

Result:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U.carrier = ⋃ i ∈ s, ↑↑i
⊢ ↑U = ↑(⨆ i, ↑↑i)

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
⊢ ∀ (i : ↑s), ↑↑i ≤ U

Tactic:
intro i

Result:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
i : ↑s
⊢ ↑↑i ≤ U

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∀ (i : ↑s), (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0

Tactic:
intro i

Result:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0