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

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'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
⊢ ⨅ I ∈ Ideal.comap (algebraMap R S) '' {J | P' ≤ J ∧ J.IsMaximal}, I ≤
    ⨅ a ∈ {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}, a

Tactic:
refine iInf_le_iInf_of_subset fun I hI => ⟨map (algebraMap R S) I, ⟨?_, ?_⟩⟩

Result:
case intro.refine_1
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'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
I : Ideal R
hI : I ∈ {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
⊢ Ideal.map (algebraMap R S) I ∈ {J | P' ≤ J ∧ J.IsMaximal}

case intro.refine_2
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'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
I : Ideal R
hI : I ∈ {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}
⊢ Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I

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'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
⊢ Ideal.comap (algebraMap R S) P'.jacobson ≤ sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}

Tactic:
rw [Ideal.jacobson, comap_sInf', sInf_eq_iInf]

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'
this : sInf {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ Ideal.comap (algebraMap R S) P'
⊢ ⨅ I ∈ Ideal.comap (algebraMap R S) '' {J | P' ≤ J ∧ J.IsMaximal}, I ≤
    ⨅ a ∈ {I | Ideal.comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}, a

Proof state:
case neg
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}
h : y ∉ J
⊢ x * y ∈ J

Tactic:
exact J.mul_mem_right y ((mem_sInf.1 hx) ⟨hJ.left, ⟨hJ.right, h⟩⟩)

Result:
no goals

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}
hxy : x * y ∈ Ideal.comap (algebraMap R S) P'
⊢ x ∈ Ideal.comap (algebraMap R S) P'

Tactic:
rcases hP'.mem_or_mem hxy with hxy | hxy

Result:
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'

case inr
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 : y ∈ Ideal.comap (algebraMap R S) P'
⊢ x ∈ 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
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

Tactic:
by_cases h : y ∈ J

Result:
case pos
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}
h : y ∈ J
⊢ x * y ∈ J

case neg
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}
h : y ∉ J
⊢ x * y ∈ J