R : Type u_2
R₂ : Type ?u.160657
K : Type ?u.160660
M : Type u_1
M₂ : Type ?u.160666
V : Type ?u.160669
S : Type ?u.160672
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 y z : M
hxy : {x} ⊆ ↑(span R {y})
hyz : {y} ⊆ ↑(span R {z})
⊢ {x} ⊆ ↑(span R {z})
R : Type u_2
R₂ : Type ?u.160657
K : Type ?u.160660
M : Type u_1
M₂ : Type ?u.160666
V : Type ?u.160669
S : Type ?u.160672
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 y z : M
hxy : x ∈ span R {y}
hyz : y ∈ span R {z}
⊢ x ∈ span R {z}
rw [← SetLike.mem_coe, ← singleton_subset_iff] at *
no goals
R : Type u_2
R₂ : Type ?u.160657
K : Type ?u.160660
M : Type u_1
M₂ : Type ?u.160666
V : Type ?u.160669
S : Type ?u.160672
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 y z : M
hxy : {x} ⊆ ↑(span R {y})
hyz : {y} ⊆ ↑(span R {z})
⊢ {x} ⊆ ↑(span R {z})
exact Submodule.subset_span_trans hxy hyz