feat: Fintype instance for an extended family of linearly independe…

…nt vectors

Mathlib/LinearAlgebra/Basis/VectorSpace.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 -/
+import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.LinearAlgebra.FreeModule.Basic
 import Mathlib.LinearAlgebra.LinearPMap
 import Mathlib.LinearAlgebra.Projection
@@ -42,6 +43,13 @@ namespace Basis
 
 section ExistsBasis
 
+noncomputable instance [Module.Finite K (span K t)]
+    (hs : LinearIndependent K ((↑) : s → V)) (hst : s ⊆ t) :
+    Fintype (hs.extend hst) := by
+  refine Classical.choice (Cardinal.lt_aleph0_iff_fintype.1 ?_)
+  rw [← rank_span_set (hs.linearIndependent_extend hst), hs.span_extend_eq_span]
+  exact Module.rank_lt_aleph0 ..
+
 /-- If `s` is a linear independent set of vectors, we can extend it to a basis. -/
 noncomputable def extend (hs : LinearIndependent K ((↑) : s → V)) :
     Basis (hs.extend (subset_univ s)) K V :=

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -1401,6 +1401,10 @@ theorem LinearIndependent.subset_span_extend (hs : LinearIndependent K (fun x =>
   let ⟨_hbt, _hsb, htb, _hli⟩ := Classical.choose_spec (exists_linearIndependent_extension hs hst)
   htb
 
+theorem LinearIndependent.span_extend_eq_span (hs : LinearIndependent K (fun x => x : s → V))
+    (hst : s ⊆ t) : span K (hs.extend hst) = span K t :=
+  le_antisymm (span_mono (hs.extend_subset hst)) (span_le.2 (hs.subset_span_extend hst))
+
 theorem LinearIndependent.linearIndependent_extend (hs : LinearIndependent K (fun x => x : s → V))
     (hst : s ⊆ t) : LinearIndependent K ((↑) : hs.extend hst → V) :=
   let ⟨_hbt, _hsb, _htb, hli⟩ := Classical.choose_spec (exists_linearIndependent_extension hs hst)