-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isJacobsonRing_localization [H : IsJacobsonRing R] : IsJacobsonRing S

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
hP : (Ideal.comap (algebraMap R S) P').jacobson = Ideal.comap (algebraMap R S) P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J | Ideal.comap (algebraMap R S) P' ≤ J ∧ J.IsMaximal} → x * y ∈ I

Tactic:
intro J hJ

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
hP : (Ideal.comap (algebraMap R S) P').jacobson = Ideal.comap (algebraMap R S) P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
J : Ideal R
hJ : J ∈ {J | Ideal.comap (algebraMap R S) P' ≤ J ∧ J.IsMaximal}
⊢ x * y ∈ J

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
hP : (Ideal.comap (algebraMap R S) P').jacobson = Ideal.comap (algebraMap R S) P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
⊢ x * y ∈ (Ideal.comap (algebraMap R S) P').jacobson

Tactic:
rw [Ideal.jacobson, Ideal.mem_sInf]

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
hP : (Ideal.comap (algebraMap R S) P').jacobson = Ideal.comap (algebraMap R S) P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J | Ideal.comap (algebraMap R S) P' ≤ J ∧ J.IsMaximal} → x * y ∈ I

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
hP : (Ideal.comap (algebraMap R S) P').jacobson = Ideal.comap (algebraMap R S) P'
x : R
hx : x ∈ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
hxy✝ : x * y ∈ Ideal.comap (algebraMap R S) P'
hxy : x ∈ Ideal.comap (algebraMap R S) P'
⊢ x ∈ Ideal.comap (algebraMap R S) P'

Tactic:
exact hxy

Result:
no goals

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
hP : (Ideal.comap (algebraMap R S) P').jacobson = Ideal.comap (algebraMap R S) P'
⊢ P'.jacobson ≤ P'

Tactic:
refine (IsLocalization.map_comap (powers y) S P'.jacobson).ge.trans
  ((map_mono ?_).trans (IsLocalization.map_comap (powers y) S P').le)

Result:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
hP : (Ideal.comap (algebraMap R S) P').jacobson = Ideal.comap (algebraMap R S) P'
⊢ Ideal.comap (algebraMap R S) P'.jacobson ≤ Ideal.comap (algebraMap R S) P'

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P

Tactic:
refine fun P' hP' => le_antisymm ?_ le_jacobson

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP' : P'.IsPrime
⊢ P'.jacobson ≤ P'

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP' : P'.IsPrime
⊢ P'.jacobson ≤ P'

Tactic:
obtain ⟨hP', hPM⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (powers y) S P').mp hP'

Result:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
y : R
inst✝¹ : Algebra R S
inst✝ : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'✝ : P'.IsPrime
hP' : (Ideal.comap (algebraMap R S) P').IsPrime
hPM : Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) P')
⊢ P'.jacobson ≤ P'