awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ IsMaximal (under R J)
have hJ₁ : 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
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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)
⊢ IsMaximal (under R J)
have this : y ∉ Submodule.toAddSubmonoid (under R J)
Tactic: have : y ∉ (J.under R).1 := Set.disjoint_left.1 hJ.right (Submonoid.mem_powers _)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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)
⊢ IsMaximal (under R J)
have this₁ : ¬∀ ⦃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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ IsMaximal (under R J)
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ IsMaximal (under R J)
have mp : ∀ (I : Ideal R) (hI' : y ∉ I) (hJI : under R J ≤ I) (hIm : I.IsMaximal), IsMaximal (under R J)
Tactic: rcases this with ⟨I, ⟨hJI, hIm⟩, hI'⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ IsMaximal (under R J)
have h₁ : Eq.{u_1 + 1} (α := Semiring R) CommSemiring.toSemiring Ring.toSemiring → under R J = I
Tactic: convert! hIm
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ under R J = I
have pos : ∀ (hJ : J = Ideal.map (F := R →+* S) (algebraMap R S) I), under R J = I
Tactic: by_cases hJ : J = I.map (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ under R J = I
have neg : ∀ (hJ : ¬J = Ideal.map (F := R →+* S) (algebraMap R S) I), under R J = I
Tactic: by_cases hJ : J = I.map (algebraMap R S)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ under R J = I
have pos : Disjoint (↑(powers y) : Set R) (↑I : Set R)
Tactic: rw [hJ, under_map_of_isPrime_disjoint (powers y) S hIm.isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)
have refine : Disjoint (↑(powers y) : Set R) (↑I : Set R)
Tactic: refine isPrime_of_isPrime_disjoint (powers y) _ I hIm.isPrime ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ under R J = I
have hI_p : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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)
⊢ under R J = I
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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) ∧ y ∉ under R J → J.IsMaximal
have mpr : IsMaximal (under R J) → ((algebraMap R S : (a : R) → S) y : S) ∉ J → J.IsMaximal
Tactic: simp only [Ideal.mem_comap, and_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ IsMaximal.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have rw : I.IsMaximal ∧ y ∉ I
Tactic: rw [isMaximal_iff_isMaximal_disjoint S y, under_map_of_isPrime_disjoint (powers y) S hI.isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ IsMaximal.{u_2} (α := S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have rw₁ : Disjoint (↑(powers y) : Set R) (↑I : Set R)
Tactic: rw [isMaximal_iff_isMaximal_disjoint S y, under_map_of_isPrime_disjoint (powers y) S hI.isPrime]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ IsJacobsonRing S
have rw : ∀ (P : Ideal S), P.IsPrime → P.jacobson = P
Tactic: rw [isJacobsonRing_iff_prime_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
have refine : ∀ (P' : Ideal S) (hP' : P'.IsPrime), P'.jacobson ≤ P'
Tactic: refine fun P' hP' => le_antisymm ?_ le_jacobson
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ P'.jacobson ≤ P'
have hP'₁ : IsPrime (under R P')
Tactic: obtain ⟨hP', hPM⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (powers y) S P').mp hP'
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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')
⊢ P'.jacobson ≤ P'
have hPM : 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'
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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)
⊢ P'.jacobson ≤ P'
have hP : Eq.{u_1 + 1} (α := Ideal R) (jacobson (under R P')) (under R P')
Tactic: have hP := H.out hP'.isRadical
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'
have refine : LE.le (α := Ideal R) (under R P'.jacobson) (under R P')
Tactic: refine (IsLocalization.map_under (powers y) S P'.jacobson).ge.trans
    ((map_mono ?_).trans (IsLocalization.map_under (powers y) S P').le)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)
have 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
Tactic: rw [Ideal.jacobson, Ideal.mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ x * y ∈ J
have pos : ∀ (h : y ∈ J), x * y ∈ J
Tactic: by_cases h : y ∈ J
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ x * y ∈ J
have neg : ∀ (h : y ∉ J), x * y ∈ J
Tactic: by_cases h : y ∈ J
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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 (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x
have hxy : 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⟩⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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 (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x
have hxy₁ : Membership.mem (γ := Ideal R) (under R P' : Ideal R) (x * y)
Tactic: rw [hP] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x
have 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
Tactic: rcases hP'.mem_or_mem hxy with hxy | hxy
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ Membership.mem (γ := Submodule R R) (Ideal.comap (F := R →+* S) (algebraMap R S) P') x
have 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
Tactic: rcases hP'.mem_or_mem hxy with hxy | hxy
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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')
⊢ LE.le (α := Ideal R) (under R P'.jacobson) (under R P')
have this : LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
  (Ideal.comap (F := R →+* S) (algebraMap R S) P')
Tactic: have : sInf { I : Ideal R | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I } ≤
      comap (algebraMap R S) P' := by
    intro x hx
    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⟩⟩)
    rw [hP] at hxy
    rcases hP'.mem_or_mem hxy with hxy | hxy
    · exact hxy
    · exact (hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
⊢ LE.le (α := Ideal R) (under R P'.jacobson) (under R P')
have refine : LE.le (α := Ideal R) (under R P'.jacobson)
  (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
Tactic: refine le_trans ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
⊢ LE.le (α := Ideal R) (under R P'.jacobson)
    (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
have rw : LE.le.{u_1} (α := Ideal R)
  (⨅ (I : Ideal R),
    ⨅ (_ :
      Membership.mem (γ := Set (Ideal R))
        (Set.image (α := Ideal S) (Ideal.comap (F := R →+* S) (algebraMap R S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal})
        I),
      I)
  (⨅ (a : Ideal R),
    ⨅ (_ :
      Membership.mem (γ := Set (Ideal R))
        {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} a),
      a)
Tactic: rw [Ideal.jacobson, under_def, comap_sInf', sInf_eq_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
⊢ LE.le.{u_1} (α := Ideal R)
    (⨅ (I : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          (Set.image (α := Ideal S) (Ideal.comap (F := R →+* S) (algebraMap R S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal})
          I),
        I)
    (⨅ (a : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} a),
        a)
have refine_1 : ∀ (I : Ideal R),
  Membership.mem (γ := Set (Ideal R))
      {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I →
    ∀ (hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I) (hIm : I.IsMaximal) (hyI : y ∉ I),
      Membership.mem (γ := Set (Ideal S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal}
        (Ideal.map (F := R →+* S) (algebraMap R S) I)
Tactic: refine iInf_le_iInf_of_subset fun I ⟨hI, hIm, hyI⟩ => ⟨map (algebraMap R S) I, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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')
this :
  LE.le (α := Ideal R) (sInf {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I})
    (Ideal.comap (F := R →+* S) (algebraMap R S) P')
refine_1 :
  ∀ (I : Ideal R),
    Membership.mem (γ := Set (Ideal R))
        {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I →
      ∀ (hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I) (hIm : I.IsMaximal) (hyI : y ∉ I),
        Membership.mem (γ := Set (Ideal S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal}
          (Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ LE.le.{u_1} (α := Ideal R)
    (⨅ (I : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          (Set.image (α := Ideal S) (Ideal.comap (F := R →+* S) (algebraMap R S)) {J : Ideal S | P' ≤ J ∧ J.IsMaximal})
          I),
        I)
    (⨅ (a : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} a),
        a)
have refine_2 : ∀ (I : Ideal R),
  Membership.mem (γ := Set (Ideal R))
      {I : Ideal R | Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} I →
    ∀ (hI : Ideal.comap (F := R →+* S) (algebraMap R S) P' ≤ I) (hIm : I.IsMaximal) (hyI : y ∉ I),
      Ideal.comap (F := R →+* S) (algebraMap R S) (Ideal.map (F := R →+* S) (algebraMap R S) I) = I
Tactic: refine iInf_le_iInf_of_subset fun I ⟨hI, hIm, hyI⟩ => ⟨map (algebraMap R S) I, ⟨?_, ?_⟩⟩