R : Type u_1
S : Type ?u.48789
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
⊢ p ≤ ⊥
R : Type u_1
S : Type ?u.48789
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
⊢ p = ⊥
rw [eq_bot_iff]
R : Type u_1
S : Type ?u.48789
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
v : M
hv : v ∈ p
⊢ v ∈ ⊥
R : Type u_1
S : Type ?u.48789
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
⊢ p ≤ ⊥
intro v hv
no goals
R : Type u_1
S : Type ?u.48789
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R M
p✝ q p : Submodule R M
inst✝ : Subsingleton { x // x ∈ p }
v : M
hv : v ∈ p
⊢ v ∈ ⊥
exact congr_arg Subtype.val (Subsingleton.elim (⟨v, hv⟩ : p) 0)