internlm/Lean-Github huggingface dataset:
Theorem: Matrix.subset_cols_notLinearIndependent_iff
Proof 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 n
⊢ ¬LinearIndependent (ι := ↑t) K (A.colSubmatrix t).colFun ↔ ∃ c, A *ᵥ c = 0 ∧ c ≠ 0 ∧ support c ⊆ t
Tactic:
rw [← rowFun_transpose, colSubmatrix_transpose, subset_rows_notLinearIndependent_iff]
Proof state after:
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 n
⊢ (∃ c, c ᵥ* Aᵀ = 0 ∧ c ≠ 0 ∧ support c ⊆ t) ↔ ∃ c, A *ᵥ c = 0 ∧ c ≠ 0 ∧ support c ⊆ t
Theorem: Matrix.subset_cols_notLinearIndependent_iff
Proof 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 n
⊢ (∃ c, c ᵥ* Aᵀ = 0 ∧ c ≠ 0 ∧ support c ⊆ t) ↔ ∃ c, A *ᵥ c = 0 ∧ c ≠ 0 ∧ support c ⊆ t
Tactic:
simp_rw [vecMul_transpose]
Proof state after:
no goals
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof 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
⊢ A.colSpace = ⊤ ↔ LinearIndependent K A.rowFun
Tactic:
rw [← not_iff_not, ← Ne, ← lt_top_iff_ne_top, ← orthSpace_lt_iff_lt, orthSpace_top,
  bot_lt_iff_ne_bot, Submodule.ne_bot_iff, Fintype.not_linearIndependent_iff]
Proof state after:
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 ∈ A.colSpace.orthSpace, x ≠ 0) ↔ ∃ g, ∑ i : m, g i • A.rowFun i = 0 ∧ ∃ i, g i ≠ 0
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof 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
⊢ (∃ x ∈ A.colSpace.orthSpace, x ≠ 0) ↔ ∃ g, ∑ i : m, g i • A.rowFun i = 0 ∧ ∃ i, g i ≠ 0
Tactic:
simp only [mem_orthSpace_iff', ne_eq, ← smul_eq_mul]
Proof state after:
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
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof 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
⊢ (∃ 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
Tactic:
refine ⟨fun ⟨x,hx,h0⟩ ↦ ⟨x, ?_, ne_iff.mp h0⟩, fun ⟨x,hx,h0⟩ ↦ ⟨x, fun y hy ↦ ?_, ne_iff.mpr h0⟩⟩
Proof state after:
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
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof state before:
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
Tactic:
apply dotProduct_eq_zero_of_mem_span hy
Proof state after:
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
⊢ ∀ z ∈ range Aᵀ.rowFun, (fun i => x i) ⬝ᵥ z = 0
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof state before:
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
⊢ ∀ z ∈ range Aᵀ.rowFun, (fun i => x i) ⬝ᵥ z = 0
Tactic:
rintro _ ⟨i,hi,rfl⟩
Proof state after:
case refine_2.intro.refl
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
i : n
⊢ (fun i => x i) ⬝ᵥ Aᵀ.rowFun i = 0
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof state before:
case refine_2.intro.refl
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
i : n
⊢ (fun i => x i) ⬝ᵥ Aᵀ.rowFun i = 0
Tactic:
convert congr_fun hx i
Proof state after:
case h.e'_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
i : n
⊢ (fun i => x i) ⬝ᵥ Aᵀ.rowFun i = (∑ i : m, x i • A.rowFun i) i
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof state before:
case h.e'_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
i : n
⊢ (fun i => x i) ⬝ᵥ Aᵀ.rowFun i = (∑ i : m, x i • A.rowFun i) i
Tactic:
simp only [dotProduct, rowFun_transpose, transpose_apply, Finset.sum_apply, Pi.smul_apply,
  smul_eq_mul]
Proof state after:
no goals
Theorem: Matrix.colSpace_eq_top_iff_linearIndependent_rows
Proof state before:
case h.e'_2.h
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
x✝ : n
⊢ (∑ i : m, x i • A.rowFun i) x✝ = ∑ x_1 : m, x x_1 • (fun x => A x x✝) x_1
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.rowSpace_eq_top_iff_linearIndependent_cols
Proof 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 n
⊢ A.rowSpace = ⊤ ↔ LinearIndependent K A.colFun
Tactic:
rw [← colSpace_transpose, colSpace_eq_top_iff_linearIndependent_rows, rowFun_transpose]
Proof state after:
no goals
Theorem: Matrix.ColBasis.rows_linearIndependent
Proof 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
ht : A.ColBasis t
hA : LinearIndependent K A.rowFun
⊢ LinearIndependent K (A.colSubmatrix t).rowFun
Tactic:
rw [← colSpace_eq_top_iff_linearIndependent_rows, Submodule.eq_top_iff']
Proof state after:
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
ht : A.ColBasis t
hA : LinearIndependent K A.rowFun
⊢ ∀ (x : m → K), x ∈ (A.colSubmatrix t).colSpace
Theorem: Matrix.ColBasis.rows_linearIndependent
Proof 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
ht : A.ColBasis t
hA : LinearIndependent K A.rowFun
⊢ ∀ (x : m → K), x ∈ (A.colSubmatrix t).colSpace
Tactic:
rw [← colSpace_eq_top_iff_linearIndependent_rows] at hA
Proof state after:
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
ht : A.ColBasis t
hA : A.colSpace = ⊤
⊢ ∀ (x : m → K), x ∈ (A.colSubmatrix t).colSpace
Theorem: Matrix.ColBasis.rows_linearIndependent
Proof 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
ht : A.ColBasis t
hA : A.colSpace = ⊤
⊢ ∀ (x : m → K), x ∈ (A.colSubmatrix t).colSpace
Tactic:
exact fun x ↦ by simp [hA ▸ ht.colSpace_eq]
Proof state after:
no goals
Theorem: Matrix.ColBasis.rows_linearIndependent
Proof 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
ht : A.ColBasis t
hA : A.colSpace = ⊤
x : m → K
⊢ x ∈ (A.colSubmatrix t).colSpace
Tactic:
simp [hA ▸ ht.colSpace_eq]
Proof state after:
no goals
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : LinearIndependent (ι := ↑t) K (A₁.colSubmatrix t).colFun
⊢ LinearIndependent (ι := ↑t) K (A₂.colSubmatrix t).colFun
Tactic:
rw [linearIndependent_iff'] at ht ⊢
Proof state after:
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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
⊢ ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₂.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
⊢ ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₂.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
Tactic:
by_contra h'
Proof state after:
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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
h' : ¬∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₂.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
⊢ False
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
h' : ¬∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₂.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
⊢ False
Tactic:
push_neg at h'
Proof state after:
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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
h' : ∃ s g, ∑ i ∈ s, g i • (A₂.colSubmatrix t).colFun i = 0 ∧ ∃ i ∈ s, g i ≠ 0
⊢ False
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof 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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
h' : ∃ s g, ∑ i ∈ s, g i • (A₂.colSubmatrix t).colFun i = 0 ∧ ∃ i ∈ s, g i ≠ 0
⊢ False
Tactic:
obtain ⟨t₀, c, hne, i₀, hit₀, hnz⟩ := h'
Proof state after:
case intro.intro.intro.intro.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
s : Set m
t✝ : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
t₀ : Finset ↑t
c : ↑t → K
hne : ∑ i ∈ t₀, c i • (A₂.colSubmatrix t).colFun i = 0
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
⊢ False
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.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
s : Set m
t✝ : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
t₀ : Finset ↑t
c : ↑t → K
hne : ∑ i ∈ t₀, c i • (A₂.colSubmatrix t).colFun i = 0
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
⊢ False
Tactic:
refine hnz <| ht t₀ c ?_ _ hit₀
Proof state after:
case intro.intro.intro.intro.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
s : Set m
t✝ : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
t₀ : Finset ↑t
c : ↑t → K
hne : ∑ i ∈ t₀, c i • (A₂.colSubmatrix t).colFun i = 0
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
⊢ ∑ i ∈ t₀, c i • (A₁.colSubmatrix t).colFun i = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.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
s : Set m
t✝ : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝ : Field K
A : Matrix m n K
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
t₀ : Finset ↑t
c : ↑t → K
hne : ∑ i ∈ t₀, c i • (A₂.colSubmatrix t).colFun i = 0
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
⊢ ∑ i ∈ t₀, c i • (A₁.colSubmatrix t).colFun i = 0
Tactic:
ext i
Proof state after:
case intro.intro.intro.intro.intro.h
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
m₁ : Type u_15
m₂ : Type u_16
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
h : A₁.rowSpace ≤ A₂.rowSpace
t : Set n
ht : ∀ (s : Finset ↑t) (g : ↑t → K), ∑ i ∈ s, g i • (A₁.colSubmatrix t).colFun i = 0 → ∀ i ∈ s, g i = 0
t₀ : Finset ↑t
c : ↑t → K
hne : ∑ i ∈ t₀, c i • (A₂.colSubmatrix t).colFun i = 0
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
⊢ (∑ i ∈ t₀, c i • (A₁.colSubmatrix t).colFun i) i = 0 i