R : Type u_2
R₂ : Type ?u.114155
K : Type ?u.114158
M : Type u_1
M₂ : Type ?u.114164
V : Type ?u.114167
S : Type ?u.114170
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
h : x ≠ 0
⊢ 0 ≠ { val := x, property := (_ : x ∈ span R {x}) }
R : Type u_2
R₂ : Type ?u.114155
K : Type ?u.114158
M : Type u_1
M₂ : Type ?u.114164
V : Type ?u.114167
S : Type ?u.114170
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
h : x ≠ 0
⊢ ∃ x_1 y, x_1 ≠ y
use 0, ⟨x, Submodule.mem_span_singleton_self x⟩
R : Type u_2
R₂ : Type ?u.114155
K : Type ?u.114158
M : Type u_1
M₂ : Type ?u.114164
V : Type ?u.114167
S : Type ?u.114170
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
h : x ≠ 0
H : 0 = { val := x, property := (_ : x ∈ span R {x}) }
⊢ False
R : Type u_2
R₂ : Type ?u.114155
K : Type ?u.114158
M : Type u_1
M₂ : Type ?u.114164
V : Type ?u.114167
S : Type ?u.114170
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
h : x ≠ 0
⊢ 0 ≠ { val := x, property := (_ : x ∈ span R {x}) }
intro H
R : Type u_2
R₂ : Type ?u.114155
K : Type ?u.114158
M : Type u_1
M₂ : Type ?u.114164
V : Type ?u.114167
S : Type ?u.114170
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
h : x ≠ 0
H : x = 0
⊢ False
R : Type u_2
R₂ : Type ?u.114155
K : Type ?u.114158
M : Type u_1
M₂ : Type ?u.114164
V : Type ?u.114167
S : Type ?u.114170
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
h : x ≠ 0
H : 0 = { val := x, property := (_ : x ∈ span R {x}) }
⊢ False
rw [eq_comm, Submodule.mk_eq_zero] at H
no goals
R : Type u_2
R₂ : Type ?u.114155
K : Type ?u.114158
M : Type u_1
M₂ : Type ?u.114164
V : Type ?u.114167
S : Type ?u.114170
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
x : M
h : x ≠ 0
H : x = 0
⊢ False
exact h H