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

State before:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝¹ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝¹
s✝¹ : Set m✝
t✝¹ : Set n✝
m : Type u_11
n : Type u_12
R✝ : Type u_13
s✝ : Set m
t✝ : Set n
A✝ B : Matrix m n R✝
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 *
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

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
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

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'
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

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 ?_ ?_
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

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
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

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 ?_
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

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
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

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
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

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

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⟩
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⟩

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⟩
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, ⋯⟩

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]
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⟩

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 _
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, ⋯⟩

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
State after:
no goals

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]
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

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]
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

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]
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

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' ↦ ?_
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

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
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

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 _
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

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

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
State after:
no goals

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
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'

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
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'

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
State after:
no goals

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⟩
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⟩

State before:
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⟩
Tactic:
simp only [Finsupp.total_apply, Pi.zero_apply] at hc ⊢
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

State before:
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
Tactic:
replace hc := congr_fun hc ⟨j, Or.inl hj⟩
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
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
j : n
hj : j ∈ t
hc : c.sum (fun i a => a • A.colSubmatrix (t ∪ t') i) ⟨j, ⋯⟩ = 0 ⟨j, ⋯⟩
⊢ c.sum (fun i a => a • A.colSubmatrix t i) ⟨j, hj⟩ = 0

State before:
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
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
j : n
hj : j ∈ t
hc : c.sum (fun i a => a • A.colSubmatrix (t ∪ t') i) ⟨j, ⋯⟩ = 0 ⟨j, ⋯⟩
⊢ c.sum (fun i a => a • A.colSubmatrix t i) ⟨j, hj⟩ = 0
Tactic:
convert hc
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
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
j : n
hj : j ∈ t
hc : c.sum (fun i a => a • A.colSubmatrix (t ∪ t') i) ⟨j, ⋯⟩ = 0 ⟨j, ⋯⟩
⊢ c.sum (fun i a => a • A.colSubmatrix t i) ⟨j, hj⟩ = c.sum (fun i a => a • A.colSubmatrix (t ∪ t') i) ⟨j, ⋯⟩

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
h0 : s.restrict (A.colSubmatrix t') = 0
c : m →₀ R
hss : ↑c.support ⊆ s ∪ s'
h' : Finsupp.filter (fun x => x ∈ s') c = 0
j : n
hj : j ∈ t
hc : c.sum (fun i a => a • A.colSubmatrix (t ∪ t') i) ⟨j, ⋯⟩ = 0 ⟨j, ⋯⟩
⊢ c.sum (fun i a => a • A.colSubmatrix t i) ⟨j, hj⟩ = c.sum (fun i a => a • A.colSubmatrix (t ∪ t') i) ⟨j, ⋯⟩
Tactic:
simp [colSubmatrix, Finsupp.sum]
State after:
no goals