exact ⟨fun ⟨c, hc, ⟨i, _, hi⟩, hcsupp⟩ ↦ ⟨c, hc, ⟨⟨i, hi⟩, hcsupp⟩⟩,
  fun ⟨c, hc, ⟨i,hi⟩, hc'⟩ ↦ ⟨c, hc, ⟨i, by_contra fun his ↦ hi (hc' _ his), hi⟩, hc'⟩⟩
case intro
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
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
s : Finset m
⊢ (∃ c, (∀ (a : n), ∑ x : m, c x * A.rowFun x a = 0) ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0) ↔
    ∃ c, (∀ (a : n), ∑ x : m, c x * A x a = 0) ∧ (∃ x, ¬c x = 0) ∧ ∀ x ∉ ↑s, c x = 0
no goals