∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [Nonempty ι] [inst_4 : Fintype ι] {b : ι → V},
  LinearIndependent K b → Fintype.card ι = Module.finrank K V → Submodule.span K (Set.range b) = ⊤