R : Type u_2
R₂ : Type ?u.131813
K : Type ?u.131816
M : Type u_3
M₂ : Type ?u.131822
V : Type ?u.131825
S✝ : Type ?u.131828
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
S : Type u_1
inst✝³ : Monoid S
inst✝² : SMul S R
inst✝¹ : MulAction S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ r • x ∈ span R {x}
R : Type u_2
R₂ : Type ?u.131813
K : Type ?u.131816
M : Type u_3
M₂ : Type ?u.131822
V : Type ?u.131825
S✝ : Type ?u.131828
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
S : Type u_1
inst✝³ : Monoid S
inst✝² : SMul S R
inst✝¹ : MulAction S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ span R {r • x} ≤ span R {x}
rw [span_le, Set.singleton_subset_iff, SetLike.mem_coe]
no goals
R : Type u_2
R₂ : Type ?u.131813
K : Type ?u.131816
M : Type u_3
M₂ : Type ?u.131822
V : Type ?u.131825
S✝ : Type ?u.131828
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
S : Type u_1
inst✝³ : Monoid S
inst✝² : SMul S R
inst✝¹ : MulAction S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ r • x ∈ span R {x}
exact smul_of_tower_mem _ _ (mem_span_singleton_self _)