theorem VectorSpaces.basis_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (v : ι → M) : (∃ (b : Module.Basis ι R M), ⇑b = v) ↔ LinearIndependent R v ∧ Submodule.span R (Set.range v) = ⊤

theorem VectorSpaces.basis_extension_lemma {K V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] (S L : Set V) (hS : ⊤ ≤ Submodule.span K S) (hL : LinearIndepOn K id L) [Fintype ↑S] [Fintype ↑L] : (∃ (ι' : Type u) (b : Module.Basis ι' K V), Set.range ⇑b ⊆ S) ∧ (∃ (ι' : Type u) (b : Module.Basis ι' K V), L ⊆ Set.range ⇑b ∧ Set.range ⇑b ⊆ L ∪ S) ∧ Fintype.card ↑L ≤ Fintype.card ↑S