no goals
R : Type ?u.37777
R₂ : Type ?u.37780
K : Type ?u.37783
M✝ : Type ?u.37786
M₂ : Type ?u.37789
V : Type ?u.37792
S : Type ?u.37795
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✝
M : Type u_1
inst✝ : AddCommGroup M
s : AddSubgroup M
⊢ toAddSubgroup (span ℤ ↑s) = s
rw [span_int_eq_addSubgroup_closure, s.closure_eq]