case h
R : Type u_2
R₂ : Type ?u.126518
K : Type ?u.126521
M : Type u_1
M₂ : Type ?u.126527
V : Type ?u.126530
S : Type ?u.126533
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
⊢ x✝ ∈ span R {0} ↔ x✝ ∈ ⊥
R : Type u_2
R₂ : Type ?u.126518
K : Type ?u.126521
M : Type u_1
M₂ : Type ?u.126527
V : Type ?u.126530
S : Type ?u.126533
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
⊢ span R {0} = ⊥
ext
no goals
case h
R : Type u_2
R₂ : Type ?u.126518
K : Type ?u.126521
M : Type u_1
M₂ : Type ?u.126527
V : Type ?u.126530
S : Type ?u.126533
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
⊢ x✝ ∈ span R {0} ↔ x✝ ∈ ⊥
simp [mem_span_singleton, eq_comm]