case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
⊢ IsUnit r
cases' exists_mul_sub_mem_of_sub_one_mem_jacobson r h with s hs
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
s : R
hs : r * s = 1
⊢ IsUnit r
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
s : R
hs : s * r - 1 ∈ ⊥
⊢ IsUnit r
rw [mem_bot, sub_eq_zero, mul_comm] at hs
no goals
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
r : R
h : r - 1 ∈ jacobson ⊥
s : R
hs : r * s = 1
⊢ IsUnit r
exact isUnit_of_mul_eq_one _ _ hs