case mp
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
⊢ Subsingleton (M ⧸ p) → p = ⊤

case mpr
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 = ⊤ → Subsingleton (M ⧸ p)
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
⊢ Subsingleton (M ⧸ p) ↔ p = ⊤
constructor
case mp
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
h : Subsingleton (M ⧸ p)
⊢ p = ⊤
case mp
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
⊢ Subsingleton (M ⧸ p) → p = ⊤
rintro h
case mp
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
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
⊢ x ∈ p
case mp
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
h : Subsingleton (M ⧸ p)
⊢ p = ⊤
refine' eq_top_iff.mpr fun x _ => _
case mp
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
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
this : x - 0 ∈ p
⊢ x ∈ p
case mp
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
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
⊢ x ∈ p
have : x - 0 ∈ p := (Submodule.Quotient.eq p).mp (Subsingleton.elim _ _)
no goals
case mp
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
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
this : x - 0 ∈ p
⊢ x ∈ p
rwa [sub_zero] at this
case mpr
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
⊢ Subsingleton (M ⧸ ⊤)
case mpr
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 = ⊤ → Subsingleton (M ⧸ p)
rintro rfl
no goals
case mpr
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
⊢ Subsingleton (M ⧸ ⊤)
infer_instance