-- Mathlib/AlgebraicGeometry/Noetherian.lean
theorem isLocallyNoetherian_of_affine_cover {ι} {S : ι → X.affineOpens}
    (hS : (⨆ i, S i : X.Opens) = ⊤)
    (hS' : ∀ i, IsNoetherianRing Γ(X, S i)) : IsLocallyNoetherian X

Proof state:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
this : IsNoetherianRing ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Tactic:
have := U.prop.isLocalization_basicOpen f

Result:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
this✝ : IsNoetherianRing ↑Γ(X, X.basicOpen f)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Proof state:
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Tactic:
induction U using of_affine_open_cover S hS with
| basicOpen U f hN =>
  have := U.prop.isLocalization_basicOpen f
  exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN
| openCover U s _ hN =>
  apply isNoetherianRing_of_away s ‹_›
  intro ⟨f, hf⟩
  have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩
  have := U.prop.isLocalization_basicOpen f
  have hEq := IsLocalization.algEquiv (.powers f) (Localization.Away f) Γ(X, X.basicOpen f)
  exact isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv
| hU => exact hS' _

Result:
no goals

Proof state:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
⊢ ∀ (s_1 : { x // x ∈ s }), IsNoetherianRing (Localization.Away ↑s_1)

Tactic:
intro ⟨f, hf⟩

Result:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Proof state:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
this✝ : IsNoetherianRing ↑Γ(X, X.basicOpen f)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Tactic:
have hEq := IsLocalization.algEquiv (.powers f) (Localization.Away f) Γ(X, X.basicOpen f)

Result:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
this✝ : IsNoetherianRing ↑Γ(X, X.basicOpen f)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
hEq : Localization.Away f ≃ₐ[↑Γ(X, ↑U)] ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Proof state:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
this✝ : IsNoetherianRing ↑Γ(X, X.basicOpen f)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
hEq : Localization.Away f ≃ₐ[↑Γ(X, ↑U)] ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Tactic:
exact isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv

Result:
no goals

Proof state:
case hU
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
i✝ : ι
⊢ IsNoetherianRing ↑Γ(X, ↑(S i✝))

Tactic:
exact hS' _

Result:
no goals

Proof state:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Tactic:
have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩

Result:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
f : ↑Γ(X, ↑U)
hf : f ∈ s
this : IsNoetherianRing ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing (Localization.Away ↑⟨f, hf⟩)

Proof state:
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsLocallyNoetherian X

Tactic:
refine ⟨fun U => ?_⟩

Result:
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Proof state:
case basicOpen
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hN : IsNoetherianRing ↑Γ(X, ↑U)
⊢ IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen f))

Tactic:
have := U.prop.isLocalization_basicOpen f

Result:
case basicOpen
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hN : IsNoetherianRing ↑Γ(X, ↑U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen f))

Proof state:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Tactic:
apply isNoetherianRing_of_away s ‹_›

Result:
case openCover
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
s : Finset ↑Γ(X, ↑U)
x✝ : Ideal.span ↑s = ⊤
hN : ∀ (f : { x // x ∈ s }), IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen ↑f))
⊢ ∀ (s_1 : { x // x ∈ s }), IsNoetherianRing (Localization.Away ↑s_1)

Proof state:
case basicOpen
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hN : IsNoetherianRing ↑Γ(X, ↑U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen f))

Tactic:
exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN

Result:
no goals