-- Mathlib/AlgebraicGeometry/Noetherian.lean
theorem isLocallyNoetherian_iff_of_affine_openCover (𝒰 : Scheme.OpenCover.{v, u} X)
    [∀ i, IsAffine (𝒰.obj i)] :
    IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), IsNoetherianRing Γ(𝒰.obj i, ⊤)

Proof state:
case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ IsLocallyNoetherian X

Tactic:
apply isLocallyNoetherian_of_affine_cover (S := fS)

Result:
case mpr.hS
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ ⨆ i, ↑(fS i) = ⊤

case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(X, ↑(fS i))

Proof state:
case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ (∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)) → IsLocallyNoetherian X

Tactic:
intro hCNoeth

Result:
case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
⊢ IsLocallyNoetherian X

Proof state:
case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
⊢ IsLocallyNoetherian X

Tactic:
let fS i : X.affineOpens := ⟨Scheme.Hom.opensRange (𝒰.map i), isAffineOpen_opensRange _⟩

Result:
case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ IsLocallyNoetherian X

Proof state:
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Tactic:
constructor

Result:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ IsLocallyNoetherian X → ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ (∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)) → IsLocallyNoetherian X

Proof state:
case mpr.hS'.f
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
⊢ ↑Γ(𝒰.obj i, ⊤) ≃+* ↑Γ(X, ↑(fS i))

Tactic:
apply CategoryTheory.Iso.commRingCatIsoToRingEquiv

Result:
case mpr.hS'.f.e
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
⊢ Γ(𝒰.obj i, ⊤) ≅ Γ(X, ↑(fS i))

Proof state:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
⊢ IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Tactic:
let U := Scheme.Hom.opensRange (𝒰.map i)

Result:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
⊢ IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Proof state:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Tactic:
apply isNoetherianRing_of_ringEquiv (R := Γ(X, U))

Result:
case mp.f
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ ↑Γ(X, U) ≃+* ↑Γ(𝒰.obj i, ⊤)

Proof state:
case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
⊢ IsNoetherianRing ↑Γ(X, ↑(fS i))

Tactic:
apply isNoetherianRing_of_ringEquiv (R := Γ(𝒰.obj i, ⊤))

Result:
case mpr.hS'.f
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
⊢ ↑Γ(𝒰.obj i, ⊤) ≃+* ↑Γ(X, ↑(fS i))

Proof state:
case mpr.hS'.f.e
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
⊢ Γ(𝒰.obj i, ⊤) ≅ Γ(X, ↑(fS i))

Tactic:
exact IsOpenImmersion.ΓIsoTop (𝒰.map i)

Result:
no goals

Proof state:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
⊢ IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Tactic:
have := h.component_noetherian ⟨U, isAffineOpen_opensRange _⟩

Result:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Proof state:
case mpr.hS
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ ⨆ i, ↑(fS i) = ⊤

Tactic:
rw [← Scheme.OpenCover.iSup_opensRange 𝒰]

Result:
no goals

Proof state:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ IsLocallyNoetherian X → ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Tactic:
intro h i

Result:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
⊢ IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)

Proof state:
case mp.f
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ ↑Γ(X, U) ≃+* ↑Γ(𝒰.obj i, ⊤)

Tactic:
apply CategoryTheory.Iso.commRingCatIsoToRingEquiv

Result:
case mp.f.e
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ Γ(X, U) ≅ Γ(𝒰.obj i, ⊤)

Proof state:
case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
⊢ ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(X, ↑(fS i))

Tactic:
intro i

Result:
case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hCNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
fS : 𝒰.J → ↑X.affineOpens := fun i => ⟨Scheme.Hom.opensRange (𝒰.map i), ⋯⟩
i : 𝒰.J
⊢ IsNoetherianRing ↑Γ(X, ↑(fS i))

Proof state:
case mp.f.e
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsLocallyNoetherian X
i : 𝒰.J
U : X.Opens := Scheme.Hom.opensRange (𝒰.map i)
this : IsNoetherianRing ↑Γ(X, ↑⟨U, ⋯⟩)
⊢ Γ(X, U) ≅ Γ(𝒰.obj i, ⊤)

Tactic:
exact (IsOpenImmersion.ΓIsoTop (𝒰.map i)).symm

Result:
no goals