case intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
s : R
hs : s * 1 * (r - 1) + s - 1 ∈ I
⊢ ∃ s, s * r - 1 ∈ I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
⊢ ∃ s, s * r - 1 ∈ I
cases' mem_jacobson_iff.1 h 1 with s hs
case intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
s : R
hs : s * 1 * (r - 1) + s - 1 ∈ I
⊢ s * r - 1 ∈ I
case intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
s : R
hs : s * 1 * (r - 1) + s - 1 ∈ I
⊢ ∃ s, s * r - 1 ∈ I
use s
no goals
case intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I : Ideal R
r : R
h : r - 1 ∈ jacobson I
s : R
hs : s * 1 * (r - 1) + s - 1 ∈ I
⊢ s * r - 1 ∈ I
simpa [mul_sub] using hs