internlm/Lean-Github huggingface dataset:
Theorem: Matrix.rows_linearIndependent_of_submatrix
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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ ∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i = 0
Tactic:
ext j
Proof state after:
case h
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = 0 j
Theorem: Matrix.rows_linearIndependent_of_submatrix
Proof state before:
case h
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = 0 j
Tactic:
convert congr_fun hc (f j)
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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = (∑ i ∈ s, c i • A.rowFun i) (f j)
Theorem: Matrix.rows_linearIndependent_of_submatrix
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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = (∑ i ∈ s, c i • A.rowFun i) (f j)
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_of_submatrix
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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ e.symm i ∈ Finset.image (⇑e.symm) s
Tactic:
simpa
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_of_submatrix
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
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = (c ∘ ⇑e) (e.symm i)
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_reindex
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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R A.rowFun
⊢ LinearIndependent R (A.submatrix ⇑em ⇑en).rowFun
Tactic:
rw [show A = (A.submatrix em en).submatrix em.symm en.symm from by simp]  at h
Proof state after:
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R ((A.submatrix ⇑em ⇑en).submatrix ⇑em.symm ⇑en.symm).rowFun
⊢ LinearIndependent R (A.submatrix ⇑em ⇑en).rowFun
Theorem: Matrix.rows_linearIndependent_reindex
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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R ((A.submatrix ⇑em ⇑en).submatrix ⇑em.symm ⇑en.symm).rowFun
⊢ LinearIndependent R (A.submatrix ⇑em ⇑en).rowFun
Tactic:
exact rows_linearIndependent_of_submatrix _ _ h
Proof state after:
no goals
Theorem: Matrix.rows_linearIndependent_reindex
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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R A.rowFun
⊢ A = (A.submatrix ⇑em ⇑en).submatrix ⇑em.symm ⇑en.symm
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.cols_linearIndependent_reindex
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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R A.colFun
⊢ LinearIndependent R (A.submatrix ⇑em ⇑en).colFun
Tactic:
convert rows_linearIndependent_reindex en em h
Proof state after:
no goals
Theorem: Matrix.linearIndependent_rows_of_upper_tri
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
hA : LinearIndependent R A.rowFun
hC : LinearIndependent R C.rowFun
⊢ LinearIndependent R (A.fromBlocks B 0 C).rowFun
Tactic:
simp_rw [linearIndependent_iff, Finsupp.total_apply] 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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
⊢ ∀ (l : m₀ ⊕ m₁ →₀ R), (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0 → l = 0
Theorem: Matrix.linearIndependent_rows_of_upper_tri
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
⊢ ∀ (l : m₀ ⊕ m₁ →₀ R), (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0 → l = 0
Tactic:
intro l hl
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
⊢ l = 0
Theorem: Matrix.linearIndependent_rows_of_upper_tri
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
hA : ∀ (l : m₀ →₀ R), (l.sum fun i a => a • A.rowFun i) = 0 → l = 0
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
⊢ l = 0
Tactic:
specialize hA (l.comapDomain Sum.inl Sum.inl_injective.injOn)
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
⊢ l = 0
Theorem: Matrix.linearIndependent_rows_of_upper_tri
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
hC : ∀ (l : m₁ →₀ R), (l.sum fun i a => a • C.rowFun i) = 0 → l = 0
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
⊢ l = 0
Tactic:
specialize hC (l.comapDomain Sum.inr Sum.inr_injective.injOn)
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
hC : ((Finsupp.comapDomain Sum.inr l ⋯).sum fun i a => a • C.rowFun i) = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
⊢ l = 0
Theorem: Matrix.linearIndependent_rows_of_upper_tri
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hl : (l.sum fun i a => a • (A.fromBlocks B 0 C).rowFun i) = 0
hA : ((Finsupp.comapDomain Sum.inl l ⋯).sum fun i a => a • A.rowFun i) = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
hC : ((Finsupp.comapDomain Sum.inr l ⋯).sum fun i a => a • C.rowFun i) = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
⊢ l = 0
Tactic:
simp only [Finsupp.sum, Finsupp.comapDomain_support, Finsupp.comapDomain_apply] at hA hC hl
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
⊢ l = 0
Theorem: Matrix.linearIndependent_rows_of_upper_tri
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
⊢ l = 0
Tactic:
specialize hA ?_
Proof state after:
l✝ : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁✝ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝¹ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B✝ : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hA : ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0 → Finsupp.comapDomain Sum.inl l ⋯ = 0
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
⊢ ∑ x ∈ l.support.preimage Sum.inl ⋯, l (Sum.inl x) • A.rowFun x = 0

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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
⊢ l = 0
Theorem: Matrix.linearIndependent_rows_of_upper_tri
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
⊢ l = 0
Tactic:
ext (i | i)
Proof state after:
case h.inl
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₀
⊢ l (Sum.inl i) = 0 (Sum.inl i)

case h.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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
⊢ l (Sum.inr i) = 0 (Sum.inr i)
Theorem: Matrix.linearIndependent_rows_of_upper_tri
Proof state before:
case h.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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
⊢ l (Sum.inr i) = 0 (Sum.inr i)
Tactic:
refine DFunLike.congr_fun (hC ?_) i
Proof state after:
case h.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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
⊢ ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0
Theorem: Matrix.linearIndependent_rows_of_upper_tri
Proof state before:
case h.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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
⊢ ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0
Tactic:
ext j
Proof state after:
case h.inr.h
l✝ : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁✝ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝¹ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B✝ : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
j : n₁
⊢ (∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x) j = 0 j
Theorem: Matrix.linearIndependent_rows_of_upper_tri
Proof state before:
case h.inr.h
l✝ : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁✝ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝¹ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B✝ : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
j : n₁
⊢ (∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x) j = 0 j
Tactic:
convert congr_fun hl (Sum.inr j)
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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₀ n₁ R
C : Matrix m₁ n₁ R
l : m₀ ⊕ m₁ →₀ R
hC : ∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x = 0 → Finsupp.comapDomain Sum.inr l ⋯ = 0
hl : ∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x = 0
hA : Finsupp.comapDomain Sum.inl l ⋯ = 0
i : m₁
j : n₁
⊢ (∑ x ∈ l.support.preimage Sum.inr ⋯, l (Sum.inr x) • C.rowFun x) j =
    (∑ x ∈ l.support, l x • (A.fromBlocks B 0 C).rowFun x) (Sum.inr j)