internlm/Lean-Github huggingface dataset:
Theorem: Matrix.rows_linearIndependent_union_of_upper_zero_block
Proof state before:
case h.e'_4.h.h.e'_4.h.a.inr.inr
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑s) R (A.submatrix s.incl t.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix s.incl tᶜ.incl = 0
e_1✝ : ({ a // a ∈ s } ⊕ { a // a ∉ s }) = (↑s ⊕ ↑sᶜ)
e_3✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t } → R) = (↑t ⊕ ↑tᶜ → R)
e_2✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t }) = (↑t ⊕ ↑tᶜ)
i : { a // a ∉ s }
j : { a // a ∉ t }
⊢ A.submatrix (⇑(Equiv.sumCompl fun x => x ∈ s)) (⇑(Equiv.sumCompl fun x => x ∈ t)) (Sum.inr i) (Sum.inr j) =
    (A.submatrix s.incl t.incl).fromBlocks 0 (A.submatrix sᶜ.incl t.incl) (A.submatrix sᶜ.incl tᶜ.incl) (Sum.inr i)
      (Sum.inr j)
Tactic:
rfl
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_union_of_lower_zero_block
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑s) R (A.submatrix s.incl t.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ LinearIndependent R A.rowFun
Tactic:
rw [← compl_compl s, ← compl_compl t] at hst
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ LinearIndependent R A.rowFun
Theorem: Matrix.rows_linearIndependent_union_of_lower_zero_block
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ LinearIndependent R A.rowFun
Tactic:
apply rows_linearIndependent_union_of_upper_zero_block hstc hst
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl tᶜᶜ.incl = 0
Theorem: Matrix.rows_linearIndependent_union_of_lower_zero_block
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl tᶜᶜ.incl = 0
Tactic:
rw [compl_compl]
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl t.incl = 0
Theorem: Matrix.rows_linearIndependent_union_of_lower_zero_block
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
inst✝ : Ring R
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl t.incl = 0
Tactic:
exact h0
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : LinearIndependent (ι := ↑s) R (A.submatrix s.incl t.incl).rowFun
h' : LinearIndependent (ι := ↑s') R (A.submatrix s'.incl t'.incl).rowFun
h0 : A.submatrix s.incl t'.incl = 0
⊢ LinearIndependent (ι := ↑(s ∪ s')) R (A.submatrix (s ∪ s').incl (t ∪ t').incl).rowFun
Tactic:
rw [submatrix_eq_restrict, linearIndependent_restrict_iff] at *
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (Finsupp.total m (↑t → R) R (A.colSubmatrix t)) l = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (Finsupp.total m (↑t' → R) R (A.colSubmatrix t')) l = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
⊢ ∀ (l : m →₀ R), (Finsupp.total m (↑(t ∪ t') → R) R (A.colSubmatrix (t ∪ t'))) l = 0 → ↑l.support ⊆ s ∪ s' → l = 0
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (Finsupp.total m (↑t → R) R (A.colSubmatrix t)) l = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (Finsupp.total m (↑t' → R) R (A.colSubmatrix t')) l = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
⊢ ∀ (l : m →₀ R), (Finsupp.total m (↑(t ∪ t') → R) R (A.colSubmatrix (t ∪ t'))) l = 0 → ↑l.support ⊆ s ∪ s' → l = 0
Tactic:
intro c (hc : _ = (0 : ↑(t ∪ t') → R)) hss
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (Finsupp.total m (↑t → R) R (A.colSubmatrix t)) l = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (Finsupp.total m (↑t' → R) R (A.colSubmatrix t')) l = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (Finsupp.total m (↑(t ∪ t') → R) R (A.colSubmatrix (t ∪ t'))) c = 0
hss : ↑c.support ⊆ s ∪ s'
⊢ c = 0
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (Finsupp.total m (↑t → R) R (A.colSubmatrix t)) l = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (Finsupp.total m (↑t' → R) R (A.colSubmatrix t')) l = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (Finsupp.total m (↑(t ∪ t') → R) R (A.colSubmatrix (t ∪ t'))) c = 0
hss : ↑c.support ⊆ s ∪ s'
⊢ c = 0
Tactic:
simp only [Finsupp.total_apply] at hc h 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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t' i) = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
⊢ c = 0
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
⊢ c = 0
Tactic:
refine h c ?_ ?_
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
⊢ (c.sum fun i a => a • A.colSubmatrix t 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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
⊢ ↑c.support ⊆ s
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
⊢ ↑c.support ⊆ s
Tactic:
rintro i hi
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
i : m
hi : i ∈ ↑c.support
⊢ i ∈ s
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
i : m
hi : i ∈ ↑c.support
⊢ i ∈ s
Tactic:
refine (hss hi).elim id <| fun his' ↦ False.elim ?_
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
i : m
hi : i ∈ ↑c.support
his' : i ∈ s'
⊢ False
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
i : m
hi : i ∈ ↑c.support
his' : i ∈ s'
⊢ False
Tactic:
rw [Finset.mem_coe, Finsupp.mem_support_iff] at hi
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
i : m
hi : c i ≠ 0
his' : i ∈ s'
⊢ False
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
i : m
hi : c i ≠ 0
his' : i ∈ s'
⊢ False
Tactic:
replace h' := DFunLike.congr_fun h' i
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
i : m
hi : c i ≠ 0
his' : i ∈ s'
h' : (Finsupp.filter (fun x => x ∈ s') c) i = 0 i
⊢ False
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
i : m
hi : c i ≠ 0
his' : i ∈ s'
h' : c i = 0 i
⊢ False
Tactic:
exact hi h'
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case specialize_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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t' i) = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
⊢ ((Finsupp.filter (fun x => x ∈ s') c).sum fun i a => a • A.colSubmatrix t' i) = 0
Tactic:
ext ⟨j,hj⟩
Proof state after:
case specialize_1.h.mk
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t' i) = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
j : n
hj : j ∈ t'
⊢ (Finsupp.filter (fun x => x ∈ s') c).sum (fun i a => a • A.colSubmatrix t' i) ⟨j, hj⟩ = 0 ⟨j, hj⟩
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case specialize_1.h.mk
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t' i) = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
j : n
hj : j ∈ t'
⊢ (Finsupp.filter (fun x => x ∈ s') c).sum (fun i a => a • A.colSubmatrix t' i) ⟨j, hj⟩ = 0 ⟨j, hj⟩
Tactic:
convert congr_fun hc ⟨j,Or.inr hj⟩
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✝
inst✝¹ : Ring R✝
R : Type u_14
inst✝ : CommSemiring R
s s' : Set m
t t' : Set n
A : Matrix m n R
h : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t i) = 0 → ↑l.support ⊆ s → l = 0
h' : ∀ (l : m →₀ R), (l.sum fun i a => a • A.colSubmatrix t' i) = 0 → ↑l.support ⊆ s' → l = 0
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hc : (c.sum fun i a => a • A.colSubmatrix (t ∪ t') i) = 0
hss : ↑c.support ⊆ s ∪ s'
j : n
hj : j ∈ t'
⊢ (Finsupp.filter (fun x => x ∈ s') c).sum (fun i a => a • A.colSubmatrix t' i) ⟨j, hj⟩ =
    c.sum (fun i a => a • A.colSubmatrix (t ∪ t') i) ⟨j, ⋯⟩