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

Proof state:
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

Tactic:
exact J.mul_mem_left x h

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')
⊢ P'.jacobson ≤ P'

Tactic:
have hP := H.out hP'.isRadical

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'
⊢ 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
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_prime_eq]

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), 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
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').jacobson
⊢ x ∈ Ideal.comap (algebraMap R S) P'

Tactic:
rw [hP] at hxy

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

Proof state:
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

Tactic:
exact IsLocalization.comap_map_of_isPrime_disjoint _ S I (IsMaximal.isPrime hI.2.1)
  ((disjoint_powers_iff_not_mem y hI.2.1.isPrime.isRadical).2 hI.2.2)

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

Tactic:
intro x hx

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

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 ≤ Ideal.comap (algebraMap R S) P'

Tactic:
refine le_trans ?_ this

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

Proof state:
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}

Tactic:
exact ⟨le_trans (le_of_eq (IsLocalization.map_comap (powers y) S P').symm) (map_mono hI.1),
  isMaximal_of_isMaximal_disjoint y _ hI.2.1 hI.2.2⟩

Result:
no goals

Proof state:
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'

Tactic:
exact (hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim

Result:
no goals