internlm/Lean-Github huggingface dataset:
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
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
Tactic:
simp only
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
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
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
Tactic:
obtain (hjs | hjs) := em (j ∈ s)
Proof state after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.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✝ : 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
hjs : j ∈ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace

case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.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✝ : 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
hjs : j ∉ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.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✝ : 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
hjs : j ∉ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Tactic:
by_contra hsp
Proof state after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.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✝ : 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
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
⊢ False
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.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✝ : 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
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
⊢ False
Tactic:
have heq := (h <| (linearIndependent_insert' hjs).2 ⟨hli, fun hsp' ↦ hsp ?_⟩) (subset_insert _ _)
Proof state after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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
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
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
heq : s = insert j s
⊢ False

case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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 : ∀ ⦃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
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
hsp' : A j ∈ span R (A '' s)
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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 : ∀ ⦃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
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
hsp' : A j ∈ span R (A '' s)
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Tactic:
rwa [image_eq_range_submatrix, span_eq_rowSpace ] at hsp'
Proof state after:
no goals
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : 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
Tactic:
have hse : LinearIndependent R (A.rowSubmatrix (insert e s)) := by
  apply hy.comp (inclusion (insert_subset he hsy)) <| inclusion_injective _
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
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ False
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : 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
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ False
Tactic:
apply ((linearIndependent_insert' hes).1 hse).2
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
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ A e ∈ span R (A '' s)
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : 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
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
⊢ A e ∈ span R (A '' s)
Tactic:
have hsp := h.symm.le.subset <| (subset_span <| mem_range_self _   : A e ∈ _)
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
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
hsp : A e ∈ ↑(A.rowSubmatrix s).rowSpace
⊢ A e ∈ span R (A '' s)
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : 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
hse : LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
hsp : A e ∈ ↑(A.rowSubmatrix s).rowSpace
⊢ A e ∈ span R (A '' s)
Tactic:
rwa [image_eq_range_submatrix, span_eq_rowSpace]
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
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
⊢ LinearIndependent (ι := ↑(insert e s)) R (A.rowSubmatrix (insert e s))
Tactic:
apply hy.comp (inclusion (insert_subset he hsy)) <| inclusion_injective _
Proof state after:
no goals
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_2
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : 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
Tactic:
rintro _ ⟨x, -, rfl⟩
Proof state after:
case refine_2.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
x : ↑s
⊢ (A.rowSubmatrix s).rowFun x ∈ range A.rowFun
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_2.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
x : ↑s
⊢ (A.rowSubmatrix s).rowFun x ∈ range A.rowFun
Tactic:
exact ⟨x, rfl⟩
Proof state after:
no goals
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.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✝ : 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
hjs : j ∈ s
⊢ A.rowFun j ∈ (A.rowSubmatrix s).rowSpace
Tactic:
apply subset_span
Proof state after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hjs : j ∈ s
⊢ A.rowFun j ∈ range (A.rowSubmatrix s).rowFun
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hjs : j ∈ s
⊢ A.rowFun j ∈ range (A.rowSubmatrix s).rowFun
Tactic:
simp only [rowFun_rowSubmatrix_eq, range_restrict, mem_image]
Proof state after:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hjs : j ∈ s
⊢ ∃ x ∈ s, A.rowFun x = A.rowFun j
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inl.a
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
hjs : j ∈ s
⊢ ∃ x ∈ s, A.rowFun x = A.rowFun j
Tactic:
exact ⟨j,hjs,rfl⟩
Proof state after:
no goals
Theorem: Matrix.rowBasis_iff_maximal_linearIndependent
Proof state before:
case refine_3.intro.intro.intro.refl.hyp.mk.intro.refl.inr.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
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
hjs : j ∉ s
hsp : A.rowFun j ∉ (A.rowSubmatrix s).rowSpace
heq : s = insert j s
⊢ False
Tactic:
exact hjs (heq.symm.subset (mem_insert _ _))
Proof state after:
no goals
Theorem: Matrix.colBasis_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.ColBasis t ↔ t ∈ maximals (fun x x_1 => x ⊆ x_1) {b | LinearIndependent (ι := ↑b) R (A.colSubmatrix b).colFun}
Tactic:
simp [ColBasis, rowBasis_iff_maximal_linearIndependent, rowFun_rowSubmatrix_eq,
  colFun_colSubmatrix_eq]
Proof state after:
no goals
Theorem: Matrix.subset_rows_notLinearIndependent_iff
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
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
⊢ ¬LinearIndependent (ι := ↑s) K (A.rowSubmatrix s).rowFun ↔ ∃ c, c ᵥ* A = 0 ∧ c ≠ 0 ∧ support c ⊆ s
Tactic:
obtain ⟨s,rfl⟩ := s.toFinite.exists_finset_coe
Proof state after:
case 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
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
s : Finset m
⊢ ¬LinearIndependent (ι := ↑↑s) K (A.rowSubmatrix ↑s).rowFun ↔ ∃ c, c ᵥ* A = 0 ∧ c ≠ 0 ∧ support c ⊆ ↑s
Theorem: Matrix.subset_rows_notLinearIndependent_iff
Proof state before:
case 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
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
s : Finset m
⊢ ¬LinearIndependent (ι := ↑↑s) K (A.rowSubmatrix ↑s).rowFun ↔ ∃ c, c ᵥ* A = 0 ∧ c ≠ 0 ∧ support c ⊆ ↑s
Tactic:
simp only [rowFun_rowSubmatrix_eq, Fintype.not_linearIndependent_restrict_iff, ne_eq,
  vecMul_eq_sum, not_imp_comm, support_subset_iff, funext_iff, Finset.sum_apply,
  Pi.smul_apply, smul_eq_mul, Pi.zero_apply, not_forall]
Proof state after:
case 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
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
s : Finset m
⊢ (∃ c, (∀ (a : n), ∑ x : m, c x * A.rowFun x a = 0) ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0) ↔
    ∃ c, (∀ (a : n), ∑ x : m, c x * A x a = 0) ∧ (∃ x, ¬c x = 0) ∧ ∀ x ∉ ↑s, c x = 0
Theorem: Matrix.subset_rows_notLinearIndependent_iff
Proof state before:
case 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
t : Set n
A✝ B : Matrix m n R
K : Type u_14
inst✝¹ : Field K
A : Matrix m n K
inst✝ : Fintype m
s : Finset m
⊢ (∃ c, (∀ (a : n), ∑ x : m, c x * A.rowFun x a = 0) ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0) ↔
    ∃ c, (∀ (a : n), ∑ x : m, c x * A x a = 0) ∧ (∃ x, ¬c x = 0) ∧ ∀ x ∉ ↑s, c x = 0
Tactic:
exact ⟨fun ⟨c, hc, ⟨i, _, hi⟩, hcsupp⟩ ↦ ⟨c, hc, ⟨⟨i, hi⟩, hcsupp⟩⟩,
  fun ⟨c, hc, ⟨i,hi⟩, hc'⟩ ↦ ⟨c, hc, ⟨i, by_contra fun his ↦ hi (hc' _ his), hi⟩, hc'⟩⟩
Proof state after:
no goals