-- 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
⊢ Ideal.comap (algebraMap R S) J = I

Tactic:
have hI_p : (I.map (algebraMap R S)).IsPrime := by
  refine isPrime_of_isPrime_disjoint (powers y) _ I hI.right.isPrime ?_
  rwa [disjoint_powers_iff_not_mem y hI.right.isPrime.isRadical]

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
⊢ Ideal.comap (algebraMap R S) J = I

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
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
⊢ (Ideal.map (algebraMap R S) I).IsPrime

Tactic:
refine isPrime_of_isPrime_disjoint (powers y) _ I hI.right.isPrime ?_

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
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

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

Tactic:
convert hI.right

Result:
case h.e'_3.h
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
⊢ Ideal.comap (algebraMap R S) J = I

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
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 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

Tactic:
have : y ∉ (comap (algebraMap R S) J).1 := Set.disjoint_left.1 hJ.right (Submonoid.mem_powers _)

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)
this : y ∉ (Ideal.comap (algebraMap R S) J).toAddSubmonoid
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

Proof state:
case h.e'_3.h
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
⊢ Ideal.comap (algebraMap R S) J = I

Tactic:
by_cases hJ : J = I.map (algebraMap R S)

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
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
⊢ Ideal.comap (algebraMap R S) J = I

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
⊢ Ideal.comap (algebraMap R S) J = I

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 : (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑(powers y) ↑(Ideal.comap (algebraMap R S) J)
this : y ∉ (Ideal.comap (algebraMap R S) J).toAddSubmonoid
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

Tactic:
erw [← H.out hJ.left.isRadical, Ideal.mem_sInf] at this

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)
this : ¬∀ ⦃I : Ideal R⦄, I ∈ {J_1 | Ideal.comap (algebraMap R S) J ≤ J_1 ∧ J_1.IsMaximal} → y ∈ I
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

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

Tactic:
rwa [map_comap (powers y) S I, Ideal.map_top] at this

Result:
no goals