no goals
ι : Type u'
ι' : Type ?u.1235297
R : Type ?u.1235300
K : Type u_1
M : Type ?u.1235306
M' : Type ?u.1235309
M'' : Type ?u.1235312
V : Type u
V' : Type ?u.1235317
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
hxs : ¬x ∈ s
⊢ (LinearIndependent K fun x => id ↑x) ∧ ¬id x ∈ span K (id '' s) ↔ (LinearIndependent K fun b => ↑b) ∧ ¬x ∈ span K s
simp