no goals
R : Type ?u.34774
R₂ : Type ?u.34777
K : Type ?u.34780
M : Type u_1
M₂ : Type ?u.34786
V : Type ?u.34789
S : Type ?u.34792
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 : AddSubmonoid M
⊢ (span ℕ ↑s).toAddSubmonoid = s
rw [span_nat_eq_addSubmonoid_closure, s.closure_eq]