awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ ∀ ⦃I : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | P ≤ J ∧ J.IsMaximal} I → x ∈ I

Tactic:
fun J hJ => hx ⟨le_trans hP.left hJ.left, hJ.right⟩

Premises used: And.right, And.left, And.intro, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ ∀ ⦃I : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | P ≤ J ∧ J.IsMaximal} I → x ∈ I

Tactic:
exact fun J hJ => hx ⟨le_trans hP.left hJ.left, hJ.right⟩

Premises used: And.left, And.intro, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ (M : Set (Ideal R)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M

Tactic:
⟨fun H _I h => eq_jacobson_iff_sInf_maximal.1 (H.out h.isRadical), fun H =>
    isJacobsonRing_iff_prime_eq.2 fun _P hP => eq_jacobson_iff_sInf_maximal.2 (H hP)⟩

Premises used: Iff.mpr, Ideal.eq_jacobson_iff_sInf_maximal, isJacobsonRing_iff_prime_eq, IsJacobsonRing.out, Ideal.IsPrime.isRadical, Iff.intro, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing R ↔
    ∀ {I : Ideal R}, I.IsPrime → ∃ (M : Set (Ideal R)), (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M

Tactic:
⟨fun H _I h => eq_jacobson_iff_sInf_maximal'.1 (H.out h.isRadical), fun H =>
    isJacobsonRing_iff_prime_eq.2 fun _P hP => eq_jacobson_iff_sInf_maximal'.2 (H hP)⟩

Premises used: Iff.mpr, isJacobsonRing_iff_prime_eq, Ideal.eq_jacobson_iff_sInf_maximal', IsJacobsonRing.out, Ideal.IsPrime.isRadical, Iff.intro, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
H : IsJacobsonRing R
I : Ideal R
⊢ I.radical = I.jacobson

Tactic:
le_antisymm (le_sInf fun _J ⟨hJ, hJ_max⟩ => (IsPrime.radical_le_iff hJ_max.isPrime).mpr hJ)
    (H.out (radical_isRadical I) ▸ jacobson_mono le_radical)

Premises used: Iff.mpr, Ideal.le_radical, Eq.rec, LE.le, Ideal.IsMaximal.isPrime, IsJacobsonRing.out, le_antisymm, Ideal.jacobson_mono, _private.0.Ideal.radical_eq_jacobson.match_1, le_sInf, Ideal.radical_isRadical, Ideal.IsPrime.radical_le_iff, Ideal.radical
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : IsArtinianRing R
⊢ IsJacobsonRing R

Tactic:
isJacobsonRing_iff_prime_eq.mpr fun _ _ ↦ jacobson_eq_self_of_isMaximal

Premises used: Iff.mpr, isJacobsonRing_iff_prime_eq, Ideal.jacobson_eq_self_of_isMaximal
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw : ∀ {I : Ideal S}, I.IsPrime → ∃ (M : Set (Ideal S)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_sInf_maximal]

Premises used: isJacobsonRing_iff_sInf_maximal
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
h :
  (∀ (J : Ideal S),
      Membership.mem (γ := Set (Ideal S))
          (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal}) J →
        J.IsMaximal ∨ J = ⊤) ∧
    p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})
⊢ ∃ (M : Set (Ideal S)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ p = sInf M

Tactic:
use map f '' { J : Ideal R | comap f p ≤ J ∧ J.IsMaximal }

Premises used: Ideal, Ideal.comap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
right : p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})
⊢ (∀ (J : Ideal S),
      Membership.mem (γ := Set (Ideal S))
          (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal}) J →
        J.IsMaximal ∨ J = ⊤) ∧
    p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})

Tactic:
use fun j ⟨J, hJ, hmap⟩ => hmap ▸ (map_eq_top_or_isMaximal_of_surjective f hf hJ.right).symm
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
⊢ p = Ideal.map f (jacobson (comap f p))

Tactic:
have : p = map f (comap f p).jacobson :=
    (IsJacobsonRing.out' _ <| hp.isRadical.comap f).symm ▸ (map_comap_of_surjective f hf p).symm
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
this : p = Ideal.map f (jacobson (comap f p))
⊢ p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})

Tactic:
this.trans (map_sInf hf fun J ⟨hJ, _⟩ => le_trans (Ideal.ker_le_comap f) hJ)

Premises used: _private.0.isJacobsonRing_of_surjective.match_2, LE.le, Ideal.ker_le_comap, Ideal.map_sInf, Eq.trans, RingHom.ker, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
this : p = Ideal.map f (jacobson (comap f p))
⊢ p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})

Tactic:
exact this.trans (map_sInf hf fun J ⟨hJ, _⟩ => le_trans (Ideal.ker_le_comap f) hJ)

Premises used: _private.0.isJacobsonRing_of_surjective.match_2, LE.le, Ideal.ker_le_comap, Ideal.map_sInf, Eq.trans, RingHom.ker, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : IsJacobsonRing R
b : R ⧸ I
x : R
h :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x : Quot (α := R) (⇑(Submodule.quotientRel I) : R → R → Prop))
⊢ ∃ (a : R),
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x :
        Quot (α := R) (⇑(Submodule.quotientRel I) : R → R → Prop))

Tactic:
use x
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : IsJacobsonRing R
b : R ⧸ I
x : R
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
    (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x : Quot (α := R) (⇑(Submodule.quotientRel I) : R → R → Prop))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : 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
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
pos : ∀ (hP_top : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤), P.jacobson = P
neg : ∀ (hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤), P.jacobson = P
⊢ P.jacobson = P

Tactic:
by_cases hP_top : comap (algebraMap R S) P = ⊤

Premises used: Algebra.algebraMap, Ideal.comap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
⊢ P.jacobson = P

Tactic:
simp [comap_eq_top_iff.1 hP_top]

Premises used: Ideal.comap_eq_top_iff, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
rwa rwa₁ rwa₂ rwa₃ : Ne (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
⊢ Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))

Tactic:
rwa [Quotient.nontrivial_iff]

Premises used: Ideal.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
⊢ Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))

Tactic:
have : Nontrivial (R ⧸ comap (algebraMap R S) P) := by rwa [Quotient.nontrivial_iff]
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
neg : Eq.{u_2 + 1} (α := Ideal (S ⧸ P)) (jacobson ⊥) ⊥
⊢ P.jacobson = P

Tactic:
rw [jacobson_eq_iff_jacobson_quotient_eq_bot]

Premises used: Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ P)) (jacobson ⊥) ⊥

Tactic:
eq_bot_of_comap_eq_bot (R := R ⧸ comap (algebraMap R S) P) ?_

Premises used: Ideal.eq_bot_of_comap_eq_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
neg :
  Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
      (jacobson ⊥))
    ⊥
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ P)) (jacobson ⊥) ⊥

Tactic:
refine eq_bot_of_comap_eq_bot (R := R ⧸ comap (algebraMap R S) P) ?_

Premises used: Ideal.eq_bot_of_comap_eq_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
neg :
  LE.le (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (sInf
      (Set.image (α := Ideal (S ⧸ P))
        (comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
        {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal}))
    (jacobson ⊥)
⊢ Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
      (jacobson ⊥))
    ⊥

Tactic:
rw [eq_bot_iff, ← jacobson_eq_iff_jacobson_quotient_eq_bot.1
    ((isJacobsonRing_iff_prime_eq.1 ‹_›) (comap (algebraMap R S) P) (comap_isPrime _ _)),
    comap_jacobson]

Premises used: isJacobsonRing_iff_prime_eq, Algebra.algebraMap, Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot, Ideal.comap, Iff.mp, Ideal.comap_isPrime, eq_bot_iff, Ideal.comap_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
⊢ LE.le (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (sInf
      (Set.image (α := Ideal (S ⧸ P))
        (comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
        {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal}))
    (jacobson ⊥)

Tactic:
sInf_le_sInf fun J hJ => ?_

Premises used: Set.Mem, sInf_le_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
neg :
  ∀ (J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (hJ :
      Membership.mem (γ :=
        Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
        {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) |
          ⊥ ≤ J ∧ J.IsMaximal}
        J),
    Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
      (Set.image (α := Ideal (S ⧸ P))
        (comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
        {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal})
      J
⊢ LE.le (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (sInf
      (Set.image (α := Ideal (S ⧸ P))
        (comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
        {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal}))
    (jacobson ⊥)

Tactic:
refine sInf_le_sInf fun J hJ => ?_

Premises used: sInf_le_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) | ⊥ ≤ J ∧ J.IsMaximal}
    J
neg :
  ∃ (x : Ideal (S ⧸ P)),
    x.IsMaximal ∧
      comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)) x =
        J
⊢ Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    (Set.image (α := Ideal (S ⧸ P))
      (comap (F :=
        RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
      {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal})
    J

Tactic:
simp only [true_and, Set.mem_image, bot_le, Set.mem_setOf_eq]

Premises used: Set.mem_image, Set.mem_setOf_eq, bot_le, true_and
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) | ⊥ ≤ J ∧ J.IsMaximal}
    J
⊢ J.IsMaximal

Tactic:
simpa using hJ
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) | ⊥ ≤ J ∧ J.IsMaximal}
    J
⊢ J.IsMaximal

Tactic:
have : J.IsMaximal := by simpa using hJ
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this_1 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) | ⊥ ≤ J ∧ J.IsMaximal}
    J
this : J.IsMaximal
⊢ ∃ (x : Ideal (S ⧸ P)),
    x.IsMaximal ∧
      comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)) x =
        J

Tactic:
exists_ideal_over_maximal_of_isIntegral J
    (comap_bot_le_of_injective _ algebraMap_quotient_injective)

Premises used: Ideal.comap_bot_le_of_injective, Ideal.algebraMap_quotient_injective, Ideal.exists_ideal_over_maximal_of_isIntegral
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
inst_2 : IsJacobsonRing R
⊢ IsJacobsonRing S

Tactic:
let _ : Algebra R S := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  isJacobsonRing_of_isIntegral (R := R)

Premises used: isJacobsonRing_of_isIntegral, Algebra.IsIntegral.mk, RingHom.toAlgebra
-- 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
mp : J.IsMaximal → IsMaximal (under R J) ∧ y ∉ under R J
mpr : IsMaximal (under R J) ∧ y ∉ under R J → J.IsMaximal
⊢ J.IsMaximal ↔ IsMaximal (under R J) ∧ y ∉ under R J

Tactic:
constructor
-- 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
⊢ J.IsMaximal → IsMaximal (under R J) ∧ y ∉ under R J

Tactic:
fun h => ⟨?_, fun hy =>
      h.ne_top (Ideal.eq_top_of_isUnit_mem _ hy (map_units _ ⟨y, Submonoid.mem_powers _⟩))⟩

Premises used: Ideal.eq_top_of_isUnit_mem, Subtype.mk, And.intro, IsLocalization.map_units, Ideal.IsMaximal.ne_top, Submonoid.mem_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
mp : ∀ (h : J.IsMaximal), IsMaximal (under R J)
⊢ J.IsMaximal → IsMaximal (under R J) ∧ y ∉ under R J

Tactic:
refine fun h => ⟨?_, fun hy =>
      h.ne_top (Ideal.eq_top_of_isUnit_mem _ hy (map_units _ ⟨y, Submonoid.mem_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
⊢ J.IsPrime

Tactic:
have hJ : J.IsPrime := IsMaximal.isPrime 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
J : Ideal S
h : J.IsMaximal
hJ : J.IsPrime
⊢ IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)

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

Premises used: IsLocalization.isPrime_iff_isPrime_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
h : J.IsMaximal
hJ : IsPrime (under R J) ∧ Disjoint (↑(powers y) : Set R) (↑(under R J) : Set R)
⊢ y ∉ Submodule.toAddSubmonoid (under R J)

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