-- Mathlib/AlgebraicGeometry/Noetherian.lean
theorem isNoetherianRing_of_away : IsNoetherianRing R

Proof state:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
⊢ ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s

Tactic:
intro s

Result:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
s : { x // x ∈ S }
⊢ minN ↑s ∈ suitableN ↑s

Proof state:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ I N = I n

Tactic:
rw [IsLocalization.ideal_eq_iInf_comap_map_away hS (I N),
    IsLocalization.ideal_eq_iInf_comap_map_away hS (I n),
    iInf_subtype', iInf_subtype']

Result:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ ⨅ x, Ideal.comap (algebraMap R (Localization.Away ↑x)) (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) =
    ⨅ x, Ideal.comap (algebraMap R (Localization.Away ↑x)) (Ideal.map (algebraMap R (Localization.Away ↑x)) (I n))

Proof state:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
s : { x // x ∈ S }
⊢ minN ↑s ∈ suitableN ↑s

Tactic:
apply Nat.sInf_mem

Result:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
s : { x // x ∈ S }
⊢ (suitableN ↑s).Nonempty

Proof state:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
⊢ ∀ (m : ℕ), N ≤ m → I N = I m

Tactic:
have hN : ∀ s : S, minN s ≤ N := fun s => Finset.le_sup s.prop

Result:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s => sInf (suitableN s)
hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : { x // x ∈ S }), minN ↑s ≤ N
⊢ ∀ (m : ℕ), N ≤ m → I N = I m

Proof state:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m

Tactic:
let suitableN s :=
  { n : ℕ | ∀ m : ℕ, n ≤ m → (Ideal.map (floc s) (I n)) = (Ideal.map (floc s) (I m)) }

Result:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m

Proof state:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m

Tactic:
let floc s := algebraMap R (Away (M := R) s)

Result:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → I n = I m