apply ((linearIndependent_insert' hes).1 hse).2
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ False
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ A e ∈ span R (A '' s)