refine ⟨fun ⟨x,hx,h0⟩ ↦ ⟨x, ?_, ne_iff.mp h0⟩, fun ⟨x,hx,h0⟩ ↦ ⟨x, fun y hy ↦ ?_, ne_iff.mpr h0⟩⟩
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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
⊢ (∃ x, (∀ y ∈ A.colSpace, ∑ x_1 : m, x x_1 • y x_1 = 0) ∧ ¬x = 0) ↔ ∃ g, ∑ i : m, g i • A.rowFun i = 0 ∧ ∃ i, ¬g i = 0
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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
x✝ : ∃ x, (∀ y ∈ A.colSpace, ∑ x_1 : m, x x_1 • y x_1 = 0) ∧ ¬x = 0
x : m → K
hx : ∀ y ∈ A.colSpace, ∑ x_1 : m, x x_1 • y x_1 = 0
h0 : ¬x = 0
⊢ ∑ i : m, x i • A.rowFun i = 0

case 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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
x✝ : ∃ g, ∑ i : m, g i • A.rowFun i = 0 ∧ ∃ i, ¬g i = 0
x : m → K
hx : ∑ i : m, x i • A.rowFun i = 0
h0 : ∃ i, ¬x i = 0
y : m → K
hy : y ∈ A.colSpace
⊢ ∑ x_1 : m, x x_1 • y x_1 = 0