[GOAL]
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = -span R s
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s
[PROOFSTEP]
rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]
[GOAL]
case a
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(span R s)
[PROOFSTEP]
exact subset_span
[GOAL]
case a
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -span R s ≤ span R (-s)
[PROOFSTEP]
rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]
[GOAL]
case a
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ ↑(span R (-s))
[PROOFSTEP]
exact subset_span
[GOAL]
α✝ : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : Monoid α✝
inst✝⁶ : DistribMulAction α✝ M
inst✝⁵ : SMulCommClass α✝ R M
α : Type u_4
inst✝⁴ : Semiring α
inst✝³ : Module α R
inst✝² : Module α M
inst✝¹ : SMulCommClass α R M
inst✝ : IsScalarTower α R M
a : α
S : Submodule R M
⊢ a • S ≤ S
[PROOFSTEP]
rintro y ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
α✝ : Type u_1
R : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : Monoid α✝
inst✝⁶ : DistribMulAction α✝ M
inst✝⁵ : SMulCommClass α✝ R M
α : Type u_4
inst✝⁴ : Semiring α
inst✝³ : Module α R
inst✝² : Module α M
inst✝¹ : SMulCommClass α R M
inst✝ : IsScalarTower α R M
a : α
S : Submodule R M
x : M
hx : x ∈ ↑S
⊢ ↑(DistribMulAction.toLinearMap R M a) x ∈ S
[PROOFSTEP]
exact smul_of_tower_mem _ a hx
