-- Mathlib/RingTheory/Localization/Ideal.lean
lemma map_radical (I : Ideal R) :
    I.radical.map (algebraMap R S) = (I.map (algebraMap R S)).radical

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : S
n : ℕ
hn : x ^ n ∈ Ideal.map (algebraMap R S) I
⊢ x ∈ Ideal.map (algebraMap R S) I.radical

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s : ↥M
hn : mk' S x s ^ n ∈ Ideal.map (algebraMap R S) I
⊢ mk' S x s ∈ Ideal.map (algebraMap R S) I.radical

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ (Ideal.map (algebraMap R S) I).radical ≤ Ideal.map (algebraMap R S) I.radical

Tactic:
rintro x ⟨n, hn⟩

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : S
n : ℕ
hn : x ^ n ∈ Ideal.map (algebraMap R S) I
⊢ x ∈ Ideal.map (algebraMap R S) I.radical

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ Ideal.map (algebraMap R S) I.radical = (Ideal.map (algebraMap R S) I).radical

Tactic:
refine (I.map_radical_le (algebraMap R S)).antisymm ?_

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ (Ideal.map (algebraMap R S) I).radical ≤ Ideal.map (algebraMap R S) I.radical

Proof state:
case h.e'_5
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ (s * x) ^ (n + 1) = s ^ n * x * (s * x ^ n)

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ ∃ s ∈ M, s * x ∈ I.radical

Tactic:
refine ⟨s, hs, n + 1, by convert I.mul_mem_left (s ^ n * x) h; ring⟩

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s : ↥M
hn : mk' S x s ^ n ∈ Ideal.map (algebraMap R S) I
⊢ mk' S x s ∈ Ideal.map (algebraMap R S) I.radical

Tactic:
simp only [← IsLocalization.mk'_pow, IsLocalization.mk'_mem_map_algebraMap_iff M,
  Submonoid.mem_powers_iff, exists_exists_eq_and] at hn ⊢

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s : ↥M
hn : ∃ s ∈ M, s * x ^ n ∈ I
⊢ ∃ s ∈ M, s * x ∈ I.radical

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ (s * x) ^ (n + 1) ∈ I

Tactic:
convert I.mul_mem_left (s ^ n * x) h

Result:
case h.e'_5
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ (s * x) ^ (n + 1) = s ^ n * x * (s * x ^ n)

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s : ↥M
hn : ∃ s ∈ M, s * x ^ n ∈ I
⊢ ∃ s ∈ M, s * x ∈ I.radical

Tactic:
obtain ⟨s, hs, h⟩ := hn

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ ∃ s ∈ M, s * x ∈ I.radical