ι : Type u'
ι' : Type ?u.1214502
R : Type ?u.1214505
K : Type u_1
M : Type ?u.1214511
M' : Type ?u.1214514
M'' : Type ?u.1214517
V : Type u
V' : Type ?u.1214522
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
⊢ LinearIndependent K (((fun o => Option.casesOn' o x v) ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      (((fun o => Option.casesOn' o x v) ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ≠ 0 ∧
        ((((fun o => Option.casesOn' o x v) ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default ∈
            span K (range (((fun o => Option.casesOn' o x v) ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl)) →
          (((fun o => Option.casesOn' o x v) ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) default = 0) ↔
    LinearIndependent K v ∧ ¬x ∈ span K (range v)
ι : Type u'
ι' : Type ?u.1214502
R : Type ?u.1214505
K : Type u_1
M : Type ?u.1214511
M' : Type ?u.1214514
M'' : Type ?u.1214517
V : Type u
V' : Type ?u.1214522
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
⊢ (LinearIndependent K fun o => Option.casesOn' o x v) ↔ LinearIndependent K v ∧ ¬x ∈ span K (range v)
rw [← linearIndependent_equiv (Equiv.optionEquivSumPUnit.{_, u'} ι).symm, linearIndependent_sum,
  @range_unique _ PUnit, @linearIndependent_unique_iff PUnit, disjoint_span_singleton]
ι : Type u'
ι' : Type ?u.1214502
R : Type ?u.1214505
K : Type u_1
M : Type ?u.1214511
M' : Type ?u.1214514
M'' : Type ?u.1214517
V : Type u
V' : Type ?u.1214522
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
h : LinearIndependent K v ∧ ¬x ∈ span K (range v)
⊢ ¬x = 0
ι : Type u'
ι' : Type ?u.1214502
R : Type ?u.1214505
K : Type u_1
M : Type ?u.1214511
M' : Type ?u.1214514
M'' : Type ?u.1214517
V : Type u
V' : Type ?u.1214522
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
⊢ (LinearIndependent K fun x => v x) ∧ ¬x = 0 ∧ (x ∈ span K (range fun x => v x) → x = 0) ↔
    LinearIndependent K v ∧ ¬x ∈ span K (range v)
refine' ⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, _, fun hx => (h.2 hx).elim⟩⟩
ι : Type u'
ι' : Type ?u.1214502
R : Type ?u.1214505
K : Type u_1
M : Type ?u.1214511
M' : Type ?u.1214514
M'' : Type ?u.1214517
V : Type u
V' : Type ?u.1214522
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z : V
h : LinearIndependent K v ∧ ¬0 ∈ span K (range v)
⊢ False
ι : Type u'
ι' : Type ?u.1214502
R : Type ?u.1214505
K : Type u_1
M : Type ?u.1214511
M' : Type ?u.1214514
M'' : Type ?u.1214517
V : Type u
V' : Type ?u.1214522
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
h : LinearIndependent K v ∧ ¬x ∈ span K (range v)
⊢ ¬x = 0
rintro rfl
no goals
ι : Type u'
ι' : Type ?u.1214502
R : Type ?u.1214505
K : Type u_1
M : Type ?u.1214511
M' : Type ?u.1214514
M'' : Type ?u.1214517
V : Type u
V' : Type ?u.1214522
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
y z : V
h : LinearIndependent K v ∧ ¬0 ∈ span K (range v)
⊢ False
exact h.2 (zero_mem _)