internlm/Lean-Github huggingface dataset:
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
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
Tactic:
simp only [colSubmatrix_transpose, rowSubmatrix_apply, Finset.sum_apply,
  Pi.smul_apply, transpose_apply, smul_eq_mul, Pi.zero_apply]
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₁
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
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₁
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Tactic:
simp only [colSubmatrix_transpose, rowSubmatrix_apply] at hne
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Tactic:
have hrs := h (subset_span <| mem_range_self i : A₁ i ∈ A₁.rowSpace)
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
hrs : A₁ i ∈ A₂.rowSpace
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
hrs : A₁ i ∈ A₂.rowSpace
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Tactic:
rw [rowSpace, mem_span_set'] at hrs
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
hrs : ∃ n_1 f g, ∑ i : Fin n_1, f i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
hrs : ∃ n_1 f g, ∑ i : Fin n_1, f i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Tactic:
obtain ⟨k, d, g, h_eq⟩ := hrs
Proof state after:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, c x * A₁ i ↑x = 0
Tactic:
simp only [← h_eq, Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Finset.mul_sum]
Proof state after:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, ∑ i : Fin k, c x * (d i * ↑(g i) ↑x) = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
⊢ ∑ x ∈ t₀, ∑ i : Fin k, c x * (d i * ↑(g i) ↑x) = 0
Tactic:
rw [Finset.sum_comm]
Proof state after:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
⊢ ∑ y : Fin k, ∑ x ∈ t₀, c x * (d y * ↑(g y) ↑x) = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
⊢ ∑ y : Fin k, ∑ x ∈ t₀, c x * (d y * ↑(g y) ↑x) = 0
Tactic:
refine Finset.sum_eq_zero (fun ind _ ↦ ?_)
Proof state after:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
⊢ ∑ x ∈ t₀, c x * (d ind * ↑(g ind) ↑x) = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
⊢ ∑ x ∈ t₀, c x * (d ind * ↑(g ind) ↑x) = 0
Tactic:
simp_rw [mul_comm (d _), ← mul_assoc, ← Finset.sum_mul]
Proof state after:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
⊢ (∑ i ∈ t₀, c i * ↑(g ind) ↑i) * d ind = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
⊢ (∑ i ∈ t₀, c i * ↑(g ind) ↑i) * d ind = 0
Tactic:
obtain ⟨_, i', hi', rfl⟩:=  g ind
Proof state after:
case intro.intro.intro.intro.intro.h.intro.intro.intro.mk.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
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ (∑ i ∈ t₀, c i * ↑⟨A₂.rowFun i', ⋯⟩ ↑i) * d ind = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.intro.intro.intro.mk.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
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ (∑ i ∈ t₀, c i * ↑⟨A₂.rowFun i', ⋯⟩ ↑i) * d ind = 0
Tactic:
simp only [mul_eq_zero]
Proof state after:
case intro.intro.intro.intro.intro.h.intro.intro.intro.mk.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
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ ∑ x ∈ t₀, c x * A₂.rowFun i' ↑x = 0 ∨ d ind = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.intro.intro.intro.mk.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
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ ∑ x ∈ t₀, c x * A₂.rowFun i' ↑x = 0 ∨ d ind = 0
Tactic:
left
Proof state after:
case intro.intro.intro.intro.intro.h.intro.intro.intro.mk.intro.refl.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ ∑ x ∈ t₀, c x * A₂.rowFun i' ↑x = 0
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
Proof state before:
case intro.intro.intro.intro.intro.h.intro.intro.intro.mk.intro.refl.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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ ∑ x ∈ t₀, c x * A₂.rowFun i' ↑x = 0
Tactic:
convert congr_fun hne 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
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ ∑ x ∈ t₀, c x * A₂.rowFun i' ↑x = (∑ x ∈ t₀, c x • A₂ᵀ ↑x) i'
Theorem: Matrix.cols_linearIndependent_of_rowSpace_le_rowSpace
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
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
i₀ : ↑t
hit₀ : i₀ ∈ t₀
hnz : c i₀ ≠ 0
i : m₁
hne : ∑ x ∈ t₀, c x • A₂ᵀ ↑x = 0
k : ℕ
d : Fin k → K
g : Fin k → ↑(range A₂.rowFun)
h_eq : ∑ i : Fin k, d i • ↑(g i) = A₁ i
ind : Fin k
x✝ : ind ∈ Finset.univ
i' : m₂
⊢ ∑ x ∈ t₀, c x * A₂.rowFun i' ↑x = (∑ x ∈ t₀, c x • A₂ᵀ ↑x) i'
Tactic:
simp
Proof state after:
no goals