exact hjs (heq.symm.subset (mem_insert _ _))
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.refine_2
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 : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
heq : s = insert j s
⊢ False
no goals