R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
hI : I ≠ ⊤
h : closure ↑I ⊆ nonunits R
⊢ Ideal.closure I ≠ ⊤
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
hI : I ≠ ⊤
⊢ Ideal.closure I ≠ ⊤
have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
hI : I ≠ ⊤
h : closure ↑I ⊆ nonunits R
⊢ Ideal.closure I ≠ ⊤
simpa only [I.closure.eq_top_iff_one, Ne.def] using mt (@h 1) one_not_mem_nonunits