case intro.intro
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 : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ Nontrivial (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
h : p < ⊤
⊢ Nontrivial (M ⧸ p)
obtain ⟨x, _, not_mem_s⟩ := SetLike.exists_of_lt h
case intro.intro
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 : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ mk x ≠ 0
case intro.intro
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 : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ Nontrivial (M ⧸ p)
refine' ⟨⟨mk x, 0, _⟩⟩
no goals
case intro.intro
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 : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : ¬x ∈ p
⊢ mk x ≠ 0
simpa using not_mem_s