∀ {M : Type u_7} {R : Type u_8} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : IsAddTorsionFree R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Module.Basis ι R M)
  (h : A = AddSubgroup.closure (Set.range ⇑b)) (i : ι), ↑((Module.Basis.addSubgroupOfClosure A b h) i) = b i