no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ 1 ∈ I
simpa only [show u.inv * x = 1 by simp] using I.mul_mem_left u.inv hxI
no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ u.inv * x = 1
simp