∀ {M : Type u_1} {R : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (A : AddSubgroup M)
  {ι : Type u_2} (b : Module.Basis ι R M),
  A = AddSubgroup.closure (Set.range ⇑b) → Submodule.span ℤ (Set.range ⇑b) = AddSubgroup.toIntSubmodule A