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

Tactic:
exact map_mono hI'

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

Tactic:
push_neg 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 ∈ {J_1 | Ideal.comap (algebraMap R S) J ≤ J_1 ∧ J_1.IsMaximal}, y ∉ I
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal

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

Tactic:
constructor

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

case mpr
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
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J → J.IsMaximal

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

Tactic:
refine fun h => ⟨⟨fun hJ => h.1.ne_top (eq_top_iff.2 ?_), fun I hI => ?_⟩⟩

Result:
case mpr.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
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.comap (algebraMap R S) J

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

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

Tactic:
refine fun hI' => hI.right ?_

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)
⊢ ↑I ⊆ ↑J

Proof state:
case mpr.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
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.comap (algebraMap R S) J

Tactic:
rwa [eq_top_iff, ← (IsLocalization.orderEmbedding (powers y) S).le_iff_le] at hJ

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

Tactic:
rcases this with ⟨I, hI, hI'⟩

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

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

Tactic:
rw [hJ, comap_map_of_isPrime_disjoint (powers y) S I (IsMaximal.isPrime hI.right)]

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

Tactic:
refine fun h => ⟨?_, fun hy =>
  h.ne_top (Ideal.eq_top_of_isUnit_mem _ hy (map_units _ ⟨y, 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
⊢ (Ideal.comap (algebraMap R S) J).IsMaximal