-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem IsLocalization.isMaximal_iff_isMaximal_disjoint [H : IsJacobsonRing R] (J : Ideal S) :
    J.IsMaximal ↔ (comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J

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
J : Ideal S
h : J.IsMaximal
hJ✝ : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) J)
I : Ideal R
hI : I ∈ {J_1 | Ideal.comap (algebraMap R S) J ≤ J_1 ∧ J_1.IsMaximal}
hI' : y ∉ I
e_2✝ : CommSemiring.toSemiring = Ring.toSemiring
hJ : ¬J = Ideal.map (algebraMap R S) I
hI_p : (Ideal.map (algebraMap R S) I).IsPrime
⊢ Ideal.comap (algebraMap R S) J = I

Tactic:
have : J ≤ I.map (algebraMap R S) := map_comap (Submonoid.powers y) S J ▸ map_mono hI.left

Result:
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
J : Ideal S
h : J.IsMaximal
hJ✝ : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) J)
I : Ideal R
hI : I ∈ {J_1 | Ideal.comap (algebraMap R S) J ≤ J_1 ∧ J_1.IsMaximal}
hI' : y ∉ I
e_2✝ : CommSemiring.toSemiring = Ring.toSemiring
hJ : ¬J = Ideal.map (algebraMap R S) I
hI_p : (Ideal.map (algebraMap R S) I).IsPrime
this : J ≤ Ideal.map (algebraMap R S) I
⊢ Ideal.comap (algebraMap R S) J = I

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
J : Ideal S
h : J.IsMaximal
hJ✝ : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) J)
I : Ideal R
hI : I ∈ {J_1 | Ideal.comap (algebraMap R S) J ≤ J_1 ∧ J_1.IsMaximal}
hI' : y ∉ I
e_2✝ : CommSemiring.toSemiring = Ring.toSemiring
hJ : ¬J = Ideal.map (algebraMap R S) I
hI_p : (Ideal.map (algebraMap R S) I).IsPrime
this : J ≤ Ideal.map (algebraMap R S) I
⊢ Ideal.comap (algebraMap R S) J = I

Tactic:
exact absurd (h.1.2 _ (lt_of_le_of_ne this hJ)) hI_p.1

Result:
no goals

Proof state:
case mp
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
J : Ideal S
h : J.IsMaximal
hJ : J.IsPrime
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

Tactic:
rw [isPrime_iff_isPrime_disjoint (Submonoid.powers y)] at hJ

Result:
case mp
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
J : Ideal S
h : J.IsMaximal
hJ : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) J)
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

Proof state:
case mpr.refine_2.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
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J
I : Ideal S
hI : J < I
hI' : ↑(Ideal.comap (algebraMap R S) I) ⊆ ↑(Ideal.comap (algebraMap R S) J)
⊢ ↑I ⊆ ↑J

Tactic:
rw [← map_comap (powers y) S I, ← map_comap (powers y) S J]

Result:
case mpr.refine_2.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
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J
I : Ideal S
hI : J < I
hI' : ↑(Ideal.comap (algebraMap R S) I) ⊆ ↑(Ideal.comap (algebraMap R S) J)
⊢ ↑(Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I)) ⊆
    ↑(Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J))

Proof state:
case mp
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
J : Ideal S
h : J.IsMaximal
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

Tactic:
have hJ : J.IsPrime := IsMaximal.isPrime h

Result:
case mp
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
J : Ideal S
h : J.IsMaximal
hJ : J.IsPrime
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

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
J : Ideal S
h : J.IsMaximal
hJ✝ : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) J)
I : Ideal R
hI : I ∈ {J_1 | Ideal.comap (algebraMap R S) J ≤ J_1 ∧ J_1.IsMaximal}
hI' : y ∉ I
e_2✝ : CommSemiring.toSemiring = Ring.toSemiring
hJ : J = Ideal.map (algebraMap R S) I
⊢ Disjoint ↑(powers y) ↑I

Tactic:
rwa [disjoint_powers_iff_not_mem y hI.right.isPrime.isRadical]

Result:
no goals

Proof state:
case mpr.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
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J
I : Ideal S
hI : J < I
⊢ I = ⊤

Tactic:
have := congr_arg (Ideal.map (algebraMap R S)) (h.1.1.2 _ ⟨comap_mono (le_of_lt hI), ?_⟩)

Result:
case mpr.refine_2.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
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J
I : Ideal S
hI : J < I
this : Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) I) = Ideal.map (algebraMap R S) ⊤
⊢ I = ⊤

case mpr.refine_2.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
J : Ideal S
h : (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J
I : Ideal S
hI : J < I
⊢ ¬↑(Ideal.comap (algebraMap R S) I) ⊆ ↑(Ideal.comap (algebraMap R S) J)