Theorem: Matrix.subset_rows_notLinearIndependent_iff (Matroid/ForMathlib/LinearAlgebra/Matrix/Rowspace.lean)

State before:
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
⊢ ¬LinearIndependent (ι := ↑s) K (A.rowSubmatrix s).rowFun ↔ ∃ c, c ᵥ* A = 0 ∧ c ≠ 0 ∧ support c ⊆ s
Tactic:
obtain ⟨s,rfl⟩ := s.toFinite.exists_finset_coe
State after:
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
⊢ ¬LinearIndependent (ι := ↑↑s) K (A.rowSubmatrix ↑s).rowFun ↔ ∃ c, c ᵥ* A = 0 ∧ c ≠ 0 ∧ support c ⊆ ↑s

State before:
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
⊢ ¬LinearIndependent (ι := ↑↑s) K (A.rowSubmatrix ↑s).rowFun ↔ ∃ c, c ᵥ* A = 0 ∧ c ≠ 0 ∧ support c ⊆ ↑s
Tactic:
simp only [rowFun_rowSubmatrix_eq, Fintype.not_linearIndependent_restrict_iff, ne_eq,
  vecMul_eq_sum, not_imp_comm, support_subset_iff, funext_iff, Finset.sum_apply,
  Pi.smul_apply, smul_eq_mul, Pi.zero_apply, not_forall]
State after:
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

State before:
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
Tactic:
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'⟩⟩
State after:
no goals