-- Mathlib/RingTheory/Localization/Ideal.lean
theorem ideal_eq_iInf_comap_map_away {S : Finset R} (hS : Ideal.span (α := R) S = ⊤) (I : Ideal R) :
    I = ⨅ f ∈ S, (I.map (algebraMap R (Localization.Away f))).comap
    (algebraMap R (Localization.Away f))

Proof state:
case a.H.mk
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
hx : x ∈ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
s : R
hs : s ∈ ↑S
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
simp only [Ideal.mem_iInf, Ideal.mem_comap] at hx

Result:
case a.H.mk
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Proof state:
case a.H.mk
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
obtain ⟨⟨y, ⟨_, n, rfl⟩⟩, e⟩ :=
  (IsLocalization.mem_map_algebraMap_iff (.powers s) _).mp (hx s hs)

Result:
case a.H.mk.intro.mk.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e :
  (algebraMap R (Localization.Away s)) x * (algebraMap R (Localization.Away s)) ↑(y, ⟨(fun x => s ^ x) n, ⋯⟩).2 =
    (algebraMap R (Localization.Away s)) ↑(y, ⟨(fun x => s ^ x) n, ⋯⟩).1
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Proof state:
case a.H.mk.intro.mk.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e : ∃ c, ↑c * (x * s ^ n) = ↑c * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
obtain ⟨⟨_, m, rfl⟩, e⟩ := e

Result:
case a.H.mk.intro.mk.mk.intro.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : ↑⟨(fun x => s ^ x) m, ⋯⟩ * (x * s ^ n) = ↑⟨(fun x => s ^ x) m, ⋯⟩ * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Proof state:
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ I = ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ I ≤ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)

case a
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ I ≤ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)

Tactic:
simp only [le_iInf₂_iff, ← Ideal.map_le_iff_le_comap, le_refl, implies_true]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : s ^ m * (x * s ^ n) = s ^ m * ↑y
⊢ s ^ m * ↑y ∈ I

Tactic:
exact I.mul_mem_left _ y.2

Result:
no goals

Proof state:
case a.H.mk.intro.mk.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e :
  (algebraMap R (Localization.Away s)) x * (algebraMap R (Localization.Away s)) ↑(y, ⟨(fun x => s ^ x) n, ⋯⟩).2 =
    (algebraMap R (Localization.Away s)) ↑(y, ⟨(fun x => s ^ x) n, ⋯⟩).1
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
dsimp only at e

Result:
case a.H.mk.intro.mk.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e :
  (algebraMap R (Localization.Away s)) x * (algebraMap R (Localization.Away s)) (s ^ n) =
    (algebraMap R (Localization.Away s)) ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
hx : x ∈ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
⊢ x ∈ I

Tactic:
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ _ hS

Result:
case a.H
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
hx : x ∈ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
⊢ ∀ (r : ↑↑S), ∃ n, ↑r ^ n • x ∈ I

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
⊢ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I) ≤ I

Tactic:
intro x hx

Result:
case a
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
hx : x ∈ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
⊢ x ∈ I

Proof state:
case a.H.mk.intro.mk.mk.intro.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : ↑⟨(fun x => s ^ x) m, ⋯⟩ * (x * s ^ n) = ↑⟨(fun x => s ^ x) m, ⋯⟩ * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
use m + n

Result:
case h
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : ↑⟨(fun x => s ^ x) m, ⋯⟩ * (x * s ^ n) = ↑⟨(fun x => s ^ x) m, ⋯⟩ * ↑y
⊢ ↑⟨s, hs⟩ ^ (m + n) • x ∈ I

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : s ^ m * (x * s ^ n) = s ^ m * ↑y
⊢ s ^ (m + n) * x ∈ I

Tactic:
rw [pow_add, mul_assoc, ← mul_comm x, e]

Result:
case h
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : s ^ m * (x * s ^ n) = s ^ m * ↑y
⊢ s ^ m * ↑y ∈ I

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : ↑⟨(fun x => s ^ x) m, ⋯⟩ * (x * s ^ n) = ↑⟨(fun x => s ^ x) m, ⋯⟩ * ↑y
⊢ ↑⟨s, hs⟩ ^ (m + n) • x ∈ I

Tactic:
dsimp at e ⊢

Result:
case h
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n m : ℕ
e : s ^ m * (x * s ^ n) = s ^ m * ↑y
⊢ s ^ (m + n) * x ∈ I