no goals
ι : Type u'
ι' : Type ?u.1249118
R : Type ?u.1249121
K : Type u_1
M : Type ?u.1249127
M' : Type ?u.1249130
M'' : Type ?u.1249133
V : Type u
V' : Type ?u.1249138
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.tail v) ∧ ¬v 0 ∈ span K (range (Fin.tail v))
rw [← linearIndependent_fin_cons, Fin.cons_self_tail]