no goals
ι : Type u'
ι' : Type ?u.1220994
R : Type ?u.1220997
K : Type u_1
M : Type ?u.1221003
M' : Type ?u.1221006
M'' : Type ?u.1221009
V : Type u
V' : Type ?u.1221014
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
v : Option ι → V
⊢ LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ ¬v none ∈ span K (range (v ∘ some))
simp only [← linearIndependent_option', Option.casesOn'_none_coe]