R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : x ∈ jacobson I
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ -p ∈ I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : x ∈ jacobson I
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * y * x + r - 1 ∈ I
rw [mul_assoc, ← mul_add_one r (y * x), hr, ← hpq, ← neg_sub, add_sub_cancel]
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : x ∈ jacobson I
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ -p ∈ I
exact I.neg_mem hpi
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ IsMaximal J}
him : I ≤ M
hm : IsMaximal M
hxm : ¬x ∈ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * i ∈ M
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ IsMaximal J}
him : I ≤ M
hm : IsMaximal M
hxm : ¬x ∈ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * -y * x + z ∈ M
rw [mul_assoc, ← mul_add_one z, neg_mul, ← sub_eq_iff_eq_add.mpr df.symm, neg_sub,
  sub_add_cancel]
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ IsMaximal J}
him : I ≤ M
hm : IsMaximal M
hxm : ¬x ∈ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * i ∈ M
exact M.mul_mem_left _ hi