no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ Set.range ↑(finsetBasis K V) = Basis.ofVectorSpaceIndex K V
rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]