no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x : R
hx : x ∈ jacobson ⊥
y z : R
hz : z * y * x + z - 1 ∈ ⊥
⊢ (x * y + 1) * z = 1
rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
x : R
h : ∀ (y : R), IsUnit (x * y + 1)
y b : R
hb : (x * y + 1) * b = 1
⊢ b * y * x + b - (x * y + 1) * b = 0
ring