internlm/Lean-Github huggingface dataset:
Theorem: Matrix.rows_linearIndependent_skew_union
Proof 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 ⊢
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
Theorem: Matrix.rows_linearIndependent_skew_union
Proof 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⟩
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
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
Theorem: Matrix.rows_linearIndependent_skew_union
Proof 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
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
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, ⋯⟩
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
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]
Proof state after:
no goals
Theorem: Matrix.RowBasis.finite
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✝¹ : DivisionRing R
inst✝ : Fintype n
hs : A.RowBasis s
⊢ s.Finite
Tactic:
have := hs.linearIndependent.finite_index
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✝¹ : DivisionRing R
inst✝ : Fintype n
hs : A.RowBasis s
this : Finite ↑s
⊢ s.Finite
Theorem: Matrix.RowBasis.finite
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✝¹ : DivisionRing R
inst✝ : Fintype n
hs : A.RowBasis s
this : Finite ↑s
⊢ s.Finite
Tactic:
exact toFinite s
Proof state after:
no goals
Theorem: Matrix.exists_rowBasis_superset
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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
⊢ ∃ s, A.RowBasis s ∧ s₀ ⊆ s
Tactic:
obtain ⟨s, hss, -, h1,h2⟩ := exists_linearIndependent_extension' hs₀ (subset_univ _)
Proof state after:
case intro.intro.intro.intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ ∃ s, A.RowBasis s ∧ s₀ ⊆ s
Theorem: Matrix.exists_rowBasis_superset
Proof state before:
case intro.intro.intro.intro
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝¹ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A✝ B : Matrix m n R
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ ∃ s, A.RowBasis s ∧ s₀ ⊆ s
Tactic:
refine ⟨s, ⟨h2, le_antisymm (span_mono ?_) ?_⟩, hss⟩
Proof state after:
case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun

case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.exists_rowBasis_superset
Proof state before:
case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Tactic:
rw [image_univ, image_eq_range_submatrix] at h1
Proof state after:
case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : range A ⊆ ↑(span R (range (A.rowSubmatrix s).rowFun))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.exists_rowBasis_superset
Proof state before:
case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : range A ⊆ ↑(span R (range (A.rowSubmatrix s).rowFun))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Tactic:
rwa [rowSpace, rowSpace, Submodule.span_le, rowFun]
Proof state after:
no goals
Theorem: Matrix.exists_rowBasis_superset
Proof state before:
case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun
Tactic:
rw [rowFun_rowSubmatrix_eq, range_restrict]
Proof state after:
case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowFun '' s ⊆ range A.rowFun
Theorem: Matrix.exists_rowBasis_superset
Proof state before:
case intro.intro.intro.intro.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✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowFun '' s ⊆ range A.rowFun
Tactic:
apply image_subset_range
Proof state after:
no goals
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
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✝ : DivisionRing R
⊢ A.RowBasis s ↔ s ∈ maximals (fun x x_1 => x ⊆ x_1) {b | LinearIndependent (ι := ↑b) R (A.rowSubmatrix b).rowFun}
Tactic:
rw [mem_maximals_setOf_iff, RowBasis, and_congr_right_iff]
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✝ : DivisionRing R
⊢ LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun →
    ((A.rowSubmatrix s).rowSpace = A.rowSpace ↔
      ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y)
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
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✝ : DivisionRing R
⊢ LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun →
    ((A.rowSubmatrix s).rowSpace = A.rowSpace ↔
      ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y)
Tactic:
refine fun hli ↦ ⟨fun h y hy hsy ↦ hsy.antisymm fun e he ↦ by_contra fun hes ↦ ?_,
    fun h ↦ le_antisymm (span_mono ?_) ?_⟩
Proof state after:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : (A.rowSubmatrix s).rowSpace = A.rowSpace
y : Set m
hy : LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun
hsy : s ⊆ y
e : m
he : e ∈ y
hes : e ∉ s
⊢ False

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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun

case refine_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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
⊢ A.rowSpace ≤ (A.rowSubmatrix s).rowSpace
Tactic:
rintro x hx
Proof state after:
case refine_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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
x : n → R
hx : x ∈ A.rowSpace
⊢ x ∈ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
x : n → R
hx : x ∈ A.rowSpace
⊢ x ∈ (A.rowSubmatrix s).rowSpace
Tactic:
obtain ⟨k, c, f, g, rfl⟩ := mem_span_set'.1 hx
Proof state after:
case refine_3.intro.intro.intro.refl
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∑ i : Fin k, c i • ↑(f i) ∈ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∑ i : Fin k, c i • ↑(f i) ∈ (A.rowSubmatrix s).rowSpace
Tactic:
apply sum_smul_mem
Proof state after:
case refine_3.intro.intro.intro.refl.hyp
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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∀ c ∈ Finset.univ, ↑(f c) ∈ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp
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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
⊢ ∀ c ∈ Finset.univ, ↑(f c) ∈ (A.rowSubmatrix s).rowSpace
Tactic:
rintro i -
Proof state after:
case refine_3.intro.intro.intro.refl.hyp
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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
⊢ ↑(f i) ∈ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp
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✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
⊢ ↑(f i) ∈ (A.rowSubmatrix s).rowSpace
Tactic:
obtain ⟨_,⟨j,hj,rfl⟩⟩ := f i
Proof state after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : DivisionRing R
hli : LinearIndependent (ι := ↑s) R (A.rowSubmatrix s).rowFun
h : ∀ ⦃y : Set m⦄, LinearIndependent (ι := ↑y) R (A.rowSubmatrix y).rowFun → s ⊆ y → s = y
k : ℕ
c : Fin k → R
f : Fin k → ↑(range A.rowFun)
hx : ∑ i : Fin k, c i • ↑(f i) ∈ A.rowSpace
i : Fin k
j : m
⊢ ↑⟨A.rowFun j, ⋯⟩ ∈ (A.rowSubmatrix s).rowSpace