no goals
ι : Type u'
ι' : Type ?u.1251029
R : Type ?u.1251032
K : Type u_1
M : Type ?u.1251038
M' : Type ?u.1251041
M'' : Type ?u.1251044
V : Type u
V' : Type ?u.1251049
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
n : ℕ
v : Fin (n + 1) → V
⊢ LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ ¬v (Fin.last n) ∈ span K (range (Fin.init v))
rw [← linearIndependent_fin_snoc, Fin.snoc_init_self]