R : Type u_2
R₂ : Type ?u.66685
K : Type ?u.66688
M : Type u_1
M₂ : Type ?u.66694
V : Type ?u.66697
S : Type ?u.66700
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 s : Set M
r : R
⊢ r • s ⊆ ↑(span R s)
R : Type u_2
R₂ : Type ?u.66685
K : Type ?u.66688
M : Type u_1
M₂ : Type ?u.66694
V : Type ?u.66697
S : Type ?u.66700
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 s : Set M
r : R
⊢ span R (r • s) ≤ span R s
rw [span_le]
case intro.intro
R : Type u_2
R₂ : Type ?u.66685
K : Type ?u.66688
M : Type u_1
M₂ : Type ?u.66694
V : Type ?u.66697
S : Type ?u.66700
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 s : Set M
r : R
x : M
hx : x ∈ s
⊢ (fun x => r • x) x ∈ ↑(span R s)
R : Type u_2
R₂ : Type ?u.66685
K : Type ?u.66688
M : Type u_1
M₂ : Type ?u.66694
V : Type ?u.66697
S : Type ?u.66700
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 s : Set M
r : R
⊢ r • s ⊆ ↑(span R s)
rintro _ ⟨x, hx, rfl⟩
no goals
case intro.intro
R : Type u_2
R₂ : Type ?u.66685
K : Type ?u.66688
M : Type u_1
M₂ : Type ?u.66694
V : Type ?u.66697
S : Type ?u.66700
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 s : Set M
r : R
x : M
hx : x ∈ s
⊢ (fun x => r • x) x ∈ ↑(span R s)
exact smul_mem (span R s) r (subset_span hx)