simp only [Finsupp.mem_support_iff, ne_eq, not_not, Finset.mem_filter, and_imp]
case h.e'_2.h.e'_6
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✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t' i) = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
j : n
hj : j ∈ t'
⊢ ∀ x ∈ Finset.filter (fun a => a ∉ s') c.support, c x * A x j = 0
case h.e'_2.h.e'_6
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✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t' i) = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
j : n
hj : j ∈ t'
⊢ ∀ (x : m), ¬c x = 0 → x ∉ s' → c x * A x j = 0