R : Type ?u.32732
R₂ : Type ?u.32735
K : Type ?u.32738
M : Type u_1
M₂ : Type ?u.32744
V : Type ?u.32747
S : Type ?u.32750
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
⊢ (span ℕ s).toAddSubmonoid ≤ AddSubmonoid.closure s
R : Type ?u.32732
R₂ : Type ?u.32735
K : Type ?u.32738
M : Type u_1
M₂ : Type ?u.32744
V : Type ?u.32747
S : Type ?u.32750
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
⊢ (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s
refine' Eq.symm (AddSubmonoid.closure_eq_of_le subset_span _)
R : Type ?u.32732
R₂ : Type ?u.32735
K : Type ?u.32738
M : Type u_1
M₂ : Type ?u.32744
V : Type ?u.32747
S : Type ?u.32750
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
⊢ span ℕ s ≤ ↑(OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule)) (AddSubmonoid.closure s)
R : Type ?u.32732
R₂ : Type ?u.32735
K : Type ?u.32738
M : Type u_1
M₂ : Type ?u.32744
V : Type ?u.32747
S : Type ?u.32750
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
⊢ (span ℕ s).toAddSubmonoid ≤ AddSubmonoid.closure s
apply (OrderIso.to_galoisConnection (AddSubmonoid.toNatSubmodule (M := M)).symm).l_le
   (a := span ℕ s) (b := AddSubmonoid.closure s)
R : Type ?u.32732
R₂ : Type ?u.32735
K : Type ?u.32738
M : Type u_1
M₂ : Type ?u.32744
V : Type ?u.32747
S : Type ?u.32750
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
⊢ s ⊆ ↑(↑(OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule)) (AddSubmonoid.closure s))
R : Type ?u.32732
R₂ : Type ?u.32735
K : Type ?u.32738
M : Type u_1
M₂ : Type ?u.32744
V : Type ?u.32747
S : Type ?u.32750
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
⊢ span ℕ s ≤ ↑(OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule)) (AddSubmonoid.closure s)
rw [span_le]
no goals
R : Type ?u.32732
R₂ : Type ?u.32735
K : Type ?u.32738
M : Type u_1
M₂ : Type ?u.32744
V : Type ?u.32747
S : Type ?u.32750
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
⊢ s ⊆ ↑(↑(OrderIso.symm (OrderIso.symm AddSubmonoid.toNatSubmodule)) (AddSubmonoid.closure s))
exact AddSubmonoid.subset_closure