no goals
R : Type ?u.1240
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule ℕ M
x✝ : FG P
S : Finset M
hS : span ℕ ↑S = P
⊢ AddSubmonoid.closure ↑S = P.toAddSubmonoid
simpa [← span_nat_eq_addSubmonoid_closure] using hS
no goals
R : Type ?u.1240
M : Type u_1
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule ℕ M
x✝ : AddSubmonoid.FG P.toAddSubmonoid
S : Finset M
hS : AddSubmonoid.closure ↑S = P.toAddSubmonoid
⊢ span ℕ ↑S = P
simpa [← span_nat_eq_addSubmonoid_closure] using hS