R : Type u_2
M : Type u_1
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p' : Submodule R M
⊢ Nonempty (Unique (M ⧸ ⊤))
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ p = ⊤ → Nonempty (Unique (M ⧸ p))
rintro rfl
no goals
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p' : Submodule R M
⊢ Nonempty (Unique (M ⧸ ⊤))
exact ⟨QuotientTop.unique⟩