∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v v_1 : ι → M} (e_v : v = v_1) (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)),
  Module.Basis.mk hli hsp = Module.Basis.mk ⋯ ⋯