awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
this : y ∉ Submodule.toAddSubmonoid (under R J)
⊢ ¬∀ ⦃I : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | under R J ≤ J_1 ∧ J_1.IsMaximal} I → y ∈ I

Tactic:
rw [← H.out hJ.left.isRadical, jacobson, Submodule.mem_toAddSubmonoid, Ideal.mem_sInf] at this

Premises used: Ideal.jacobson, Ideal.mem_sInf, IsJacobsonRing.out, Submodule.mem_toAddSubmonoid, And.left, Ideal.IsPrime.isRadical
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
this : ¬∀ ⦃I : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | under R J ≤ J_1 ∧ J_1.IsMaximal} I → y ∈ I
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | under R J ≤ J_1 ∧ J_1.IsMaximal} I ∧ y ∉ I

Tactic:
push Not at this

Premises used: Not
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
this : ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | under R J ≤ J_1 ∧ J_1.IsMaximal} I ∧ y ∉ I
mp : ∀ (I : Ideal R) (hI' : y ∉ I) (hJI : under R J ≤ I) (hIm : I.IsMaximal), IsMaximal (under R J)
⊢ IsMaximal (under R J)

Tactic:
rcases this with ⟨I, ⟨hJI, hIm⟩, hI'⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
⊢ I.IsMaximal

Tactic:
hIm
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
h₁ : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring → under R J = I
⊢ IsMaximal (under R J)

Tactic:
convert! hIm
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
pos : ∀ (hJ : J = Ideal.map (F := R →+* S) (algebraMap R S) I), under R J = I
neg : ∀ (hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I), under R J = I
⊢ under R J = I

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

Premises used: Algebra.algebraMap, Ideal.map
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : J = Ideal.map (F := R →+* S) (algebraMap R S) I
pos : Disjoint (↑(powers y) : Set R) (↑I : Set R)
⊢ under R J = I

Tactic:
rw [hJ, under_map_of_isPrime_disjoint (powers y) S hIm.isPrime]

Premises used: Ideal.IsMaximal.isPrime, Submonoid.powers, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : J = Ideal.map (F := R →+* S) (algebraMap R S) I
pos pos₁ pos₂ pos₃ : y ∉ I
⊢ Disjoint (↑(powers y) : Set R) (↑I : Set R)

Tactic:
rwa [disjoint_powers_iff_notMem_of_isPrime]

Premises used: Ideal.disjoint_powers_iff_notMem_of_isPrime
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I
⊢ IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
isPrime_of_isPrime_disjoint (powers y) _ I hIm.isPrime ?_

Premises used: IsLocalization.isPrime_of_isPrime_disjoint, Ideal.IsMaximal.isPrime, Submonoid.powers
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I
refine : Disjoint (↑(powers y) : Set R) (↑I : Set R)
⊢ IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

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

Premises used: IsLocalization.isPrime_of_isPrime_disjoint, Ideal.IsMaximal.isPrime, Submonoid.powers
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I
rwa rwa₁ rwa₂ rwa₃ : y ∉ I
⊢ Disjoint (↑(powers y) : Set R) (↑I : Set R)

Tactic:
rwa [disjoint_powers_iff_notMem_of_isPrime]

Premises used: Ideal.disjoint_powers_iff_notMem_of_isPrime
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I
⊢ IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
have hI_p : (I.map (algebraMap R S)).IsPrime := by
        refine isPrime_of_isPrime_disjoint (powers y) _ I hIm.isPrime ?_
        rwa [disjoint_powers_iff_notMem_of_isPrime]
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I
hI_p : IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ J ≤ Ideal.map (F := R →+* S) (algebraMap R S) I

Tactic:
have : J ≤ I.map (algebraMap R S) := map_under (Submonoid.powers y) S J ▸ map_mono hJI
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I
hI_p : IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
this : J ≤ Ideal.map (F := R →+* S) (algebraMap R S) I
⊢ under R J = I

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

Premises used: absurd, And.right, Ideal.IsMaximal.out, Ideal.IsPrime.ne_top', lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
hJ_1 : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
I : Ideal R
hI' : y ∉ I
hJI : under R J ≤ I
hIm : I.IsMaximal
e_2 : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring
hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I
hI_p : IsPrime.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
this : J ≤ Ideal.map (F := R →+* S) (algebraMap R S) I
⊢ under R J = I

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

Premises used: absurd, And.right, Ideal.IsMaximal.out, Ideal.IsPrime.ne_top', lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
mpr : IsMaximal (under R J) → ((algebraMap R S : (a : R) → S) y : S) ∉ J → J.IsMaximal
⊢ IsMaximal (under R J) ∧ y ∉ under R J → J.IsMaximal

Tactic:
simp only [Ideal.mem_comap, and_imp]

Premises used: and_imp, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ IsMaximal (under R J) → ((algebraMap R S : (a : R) → S) y : S) ∉ J → J.IsMaximal

Tactic:
(fun _ _ ↦ IsMaximal.of_isLocalization_of_disjoint (powers y))

Premises used: Ideal.IsMaximal.of_isLocalization_of_disjoint, Submonoid.powers
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ IsMaximal (under R J) → ((algebraMap R S : (a : R) → S) y : S) ∉ J → J.IsMaximal

Tactic:
exact (fun _ _ ↦ IsMaximal.of_isLocalization_of_disjoint (powers y))

Premises used: Ideal.IsMaximal.of_isLocalization_of_disjoint, Submonoid.powers
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
inst_4 : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
rw : I.IsMaximal ∧ y ∉ I
rw₁ : Disjoint (↑(powers y) : Set R) (↑I : Set R)
⊢ IsMaximal.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
rw [isMaximal_iff_isMaximal_disjoint S y, under_map_of_isPrime_disjoint (powers y) S hI.isPrime]

Premises used: IsLocalization.isMaximal_iff_isMaximal_disjoint, Ideal.IsMaximal.isPrime, Submonoid.powers, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
inst_4 : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ I.IsMaximal ∧ y ∉ I

Tactic:
⟨hI, hy⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
inst_4 : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy : y ∉ I
⊢ I.IsMaximal ∧ y ∉ I

Tactic:
exact ⟨hI, hy⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
inst_4 : IsJacobsonRing R
I : Ideal R
hI : I.IsMaximal
hy rwa rwa₁ rwa₂ rwa₃ : y ∉ I
⊢ Disjoint (↑(powers y) : Set R) (↑I : Set R)

Tactic:
rwa [disjoint_powers_iff_notMem_of_isPrime]

Premises used: Ideal.disjoint_powers_iff_notMem_of_isPrime
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
rw : ∀ (P : Ideal S), P.IsPrime → P.jacobson = P
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_prime_eq]

Premises used: isJacobsonRing_iff_prime_eq
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P

Tactic:
fun P' hP' => le_antisymm ?_ le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
refine : ∀ (P' : Ideal S) (hP' : P'.IsPrime), P'.jacobson ≤ P'
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P

Tactic:
refine fun P' hP' => le_antisymm ?_ le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP' : P'.IsPrime
⊢ IsPrime (under R P')

Tactic:
obtain ⟨hP', hPM⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (powers y) S P').mp hP'

Premises used: IsLocalization.isPrime_iff_isPrime_disjoint, Submonoid.powers, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP' : P'.IsPrime
hP'₁ : IsPrime (under R P')
⊢ Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)

Tactic:
obtain ⟨hP', hPM⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (powers y) S P').mp hP'

Premises used: IsLocalization.isPrime_iff_isPrime_disjoint, Submonoid.powers, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
⊢ Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')

Tactic:
have hP := H.out hP'.isRadical
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
⊢ P'.jacobson ≤ P'

Tactic:
(IsLocalization.map_under (powers y) S P'.jacobson).ge.trans
    ((map_mono ?_).trans (IsLocalization.map_under (powers y) S P').le)

Premises used: Eq.ge, Set.Mem, Ideal.jacobson, Eq.le, IsLocalization.map_under, Submonoid.powers, Ideal.map_mono, LE.le.trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
refine : LE.le (α := Ideal R) (under R P'.jacobson) (under R P')
⊢ P'.jacobson ≤ P'

Tactic:
refine (IsLocalization.map_under (powers y) S P'.jacobson).ge.trans
    ((map_mono ?_).trans (IsLocalization.map_under (powers y) S P').le)

Premises used: Eq.ge, Ideal.jacobson, Eq.le, IsLocalization.map_under, Submonoid.powers, Ideal.map_mono, LE.le.trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
rw :
  ∀ ⦃I : Ideal R⦄,
    Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ J ∧ J.IsMaximal}
        I →
      x * y ∈ I
⊢ Membership.mem (γ := Ideal R) (jacobson (Ideal.comap (F := R →+* S) (algebraMap R S) P')) (x * y)

Tactic:
rw [Ideal.jacobson, Ideal.mem_sInf]

Premises used: Ideal.jacobson, Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
J : Ideal R
hJ :
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ J ∧ J.IsMaximal} J
pos : ∀ (h : y ∈ J), x * y ∈ J
neg : ∀ (h : y ∉ J), x * y ∈ J
⊢ x * y ∈ J

Tactic:
by_cases h : y ∈ J
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
J : Ideal R
hJ :
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ J ∧ J.IsMaximal} J
h : y ∈ J
⊢ x * y ∈ J

Tactic:
J.mul_mem_left x h

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
J : Ideal R
hJ :
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ J ∧ J.IsMaximal} J
h : y ∈ J
⊢ x * y ∈ J

Tactic:
exact J.mul_mem_left x h

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
J : Ideal R
hJ :
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ J ∧ J.IsMaximal} J
h : y ∉ J
⊢ x * y ∈ J

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

Premises used: Set.Mem, Ideal.mem_sInf, And.right, And.left, Ideal.mul_mem_right, And.intro, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
J : Ideal R
hJ :
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ J ∧ J.IsMaximal} J
h : y ∉ J
⊢ x * y ∈ J

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

Premises used: Ideal.mem_sInf, And.right, And.left, Ideal.mul_mem_right, And.intro, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
⊢ Membership.mem (γ := Ideal R) (jacobson (Ideal.comap (F := R →+* S) (algebraMap R S) P')) (x * y)

Tactic:
have hxy : x * y ∈ (comap (algebraMap R S) P').jacobson := by
      rw [Ideal.jacobson, Ideal.mem_sInf]
      intro J hJ
      by_cases h : y ∈ J
      · exact J.mul_mem_left x h
      · exact J.mul_mem_right y ((mem_sInf.1 hx) ⟨hJ.left, ⟨hJ.right, h⟩⟩)
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
hxy : Membership.mem (γ := Ideal R) (jacobson (Ideal.comap (F := R →+* S) (algebraMap R S) P')) (x * y)
⊢ Membership.mem (γ := Ideal R) (under R P' : Ideal R) (x * y)

Tactic:
rw [hP] at hxy
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
P' : Ideal S
hP'_1 : P'.IsPrime
hP' : IsPrime (under R P')
hPM : Disjoint (↑(powers y) : Set R) (↑(under R P') : Set R)
hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I}) x
hxy : Membership.mem (γ := Ideal R) (under R P' : Ideal R) (x * y)
inl :
  ∀ (hxy : Membership.mem (γ := Ideal R) (under R P') x),
    Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x
inr :
  ∀ (hxy : Membership.mem (γ := Ideal R) (under R P') y),
    Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x

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

Premises used: Ideal.IsPrime.mem_or_mem