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

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

Tactic:
apply (isLocallyNoetherian_iff_of_affine_openCover _).mp

Result:
case mp.a
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.J
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsNoetherian X
i : 𝒰.J
⊢ IsLocallyNoetherian X

Proof state:
case mpr.convert_3
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.J
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
exact Scheme.OpenCover.compactSpace 𝒰

Result:
no goals

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

Tactic:
exact (isLocallyNoetherian_iff_of_affine_openCover _).mpr hNoeth

Result:
no goals

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

Tactic:
intro hNoeth

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

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

Tactic:
convert IsNoetherian.mk

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

case mpr.convert_3
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.J
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
hNoeth : ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
⊢ CompactSpace ↑↑X.toPresheafedSpace

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

Tactic:
intro h i

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

Proof state:
case mp.a
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.J
inst✝ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
h : IsNoetherian X
i : 𝒰.J
⊢ IsLocallyNoetherian X

Tactic:
exact h.toIsLocallyNoetherian

Result:
no goals

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

Tactic:
constructor

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

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