internlm/Lean-Github huggingface dataset:
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
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 ∪ t') i) +
        (Finsupp.filter (fun a => a ∉ s') c).sum fun i a => a • A.colSubmatrix (t ∪ t') i)
      ⟨j, ⋯⟩ =
    (Finsupp.filter (fun x => x ∈ s') c).sum (fun i a => a • A.colSubmatrix t' i) ⟨j, hj⟩
Tactic:
simp only [Pi.add_apply, Finsupp.sum_filter_index]
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'
⊢ (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩ +
      (∑ x ∈ (Finsupp.filter (fun a => a ∉ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩ =
    (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix t' x) ⟨j, hj⟩
Theorem: Matrix.rows_linearIndependent_skew_union
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✝
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'
⊢ (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩ +
      (∑ x ∈ (Finsupp.filter (fun a => a ∉ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩ =
    (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix t' x) ⟨j, hj⟩
Tactic:
convert add_zero _
Proof state after:
case h.e'_2.h.e'_6
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'
⊢ (∑ x ∈ (Finsupp.filter (fun a => a ∉ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩ = 0

case h.e'_3
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'
⊢ (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix t' x) ⟨j, hj⟩ =
    (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_3
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'
⊢ (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix t' x) ⟨j, hj⟩ =
    (∑ x ∈ (Finsupp.filter (fun x => x ∈ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_2.h.e'_6
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'
⊢ (∑ x ∈ (Finsupp.filter (fun a => a ∉ s') c).support, c x • A.colSubmatrix (t ∪ t') x) ⟨j, ⋯⟩ = 0
Tactic:
simp only [Finset.sum_apply, Finsupp.support_filter,
  Finsupp.mem_support_iff, ne_eq, not_not, Pi.smul_apply, colSubmatrix_apply, smul_eq_mul]
Proof state after:
case h.e'_2.h.e'_6
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'
⊢ ∑ x ∈ Finset.filter (fun a => a ∉ s') c.support, c x * A x j = 0
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_2.h.e'_6
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'
⊢ ∑ x ∈ Finset.filter (fun a => a ∉ s') c.support, c x * A x j = 0
Tactic:
rw [Finset.sum_eq_zero]
Proof state after:
case h.e'_2.h.e'_6
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'
⊢ ∀ x ∈ Finset.filter (fun a => a ∉ s') c.support, c x * A x j = 0
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_2.h.e'_6
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'
⊢ ∀ x ∈ Finset.filter (fun a => a ∉ s') c.support, c x * A x j = 0
Tactic:
simp only [Finsupp.mem_support_iff, ne_eq, not_not, Finset.mem_filter, and_imp]
Proof state after:
case h.e'_2.h.e'_6
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'
⊢ ∀ (x : m), ¬c x = 0 → x ∉ s' → c x * A x j = 0
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_2.h.e'_6
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'
⊢ ∀ (x : m), ¬c x = 0 → x ∉ s' → c x * A x j = 0
Tactic:
refine fun i hi0 his' ↦ ?_
Proof state after:
case h.e'_2.h.e'_6
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'
i : m
hi0 : ¬c i = 0
his' : i ∉ s'
⊢ c i * A i j = 0
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_2.h.e'_6
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'
i : m
hi0 : ¬c i = 0
his' : i ∉ s'
⊢ c i * A i j = 0
Tactic:
have his : i ∈ s := Or.elim (hss (show i ∈ c.support from by simpa)) id his'.elim
Proof state after:
case h.e'_2.h.e'_6
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'
i : m
hi0 : ¬c i = 0
his' : i ∉ s'
his : i ∈ s
⊢ c i * A i j = 0
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_2.h.e'_6
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'
i : m
hi0 : ¬c i = 0
his' : i ∉ s'
his : i ∈ s
⊢ c i * A i j = 0
Tactic:
convert mul_zero _
Proof state after:
case h.e'_2.h.e'_6
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'
i : m
hi0 : ¬c i = 0
his' : i ∉ s'
his : i ∈ s
⊢ A i j = 0
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case h.e'_2.h.e'_6
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'
i : m
hi0 : ¬c i = 0
his' : i ∉ s'
his : i ∈ s
⊢ A i j = 0
Tactic:
exact congr_fun (congr_fun h0 ⟨i, his⟩) ⟨j, hj⟩
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 : ∀ (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'
i : m
hi0 : ¬c i = 0
his' : i ∉ s'
⊢ i ∈ c.support
Tactic:
simpa
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case specialize_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'
⊢ ↑(Finsupp.filter (fun x => x ∈ s') c).support ⊆ s'
Tactic:
rintro x hx
Proof state after:
case specialize_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'
x : m
hx : x ∈ ↑(Finsupp.filter (fun x => x ∈ s') c).support
⊢ x ∈ s'
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case specialize_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'
x : m
hx : x ∈ ↑(Finsupp.filter (fun x => x ∈ s') c).support
⊢ x ∈ s'
Tactic:
simp only [Finsupp.support_filter, Finsupp.mem_support_iff, ne_eq, Finset.coe_filter,
  mem_setOf_eq] at hx
Proof state after:
case specialize_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'
x : m
hx : ¬c x = 0 ∧ x ∈ s'
⊢ x ∈ s'
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
case specialize_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'
x : m
hx : ¬c x = 0 ∧ x ∈ s'
⊢ x ∈ s'
Tactic:
exact hx.2
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_skew_union
Proof state before:
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
Tactic:
ext ⟨j,hj⟩
Proof state after:
case refine_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
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
j : n
hj : j ∈ t
⊢ c.sum (fun i a => a • A.colSubmatrix t i) ⟨j, hj⟩ = 0 ⟨j, hj⟩