no goals
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
⊢ Subsingleton (R ⧸ I) ↔ I = ⊤
rw [eq_top_iff_one, ← subsingleton_iff_zero_eq_one, eq_comm, ← (mk I).map_one,
  Quotient.eq_zero_iff_mem]