R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsLocal I
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsLocal I
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ r * x - 1 ∈ I
rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel]
no goals
R : Type u
S : Type v
inst✝ : CommRing R
I : Ideal R
hi : IsLocal I
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I
exact I.neg_mem hpi