internlm/Lean-Github huggingface dataset:
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
h : A₁.rowSpace = A₂.nullSpace
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
hb₂ : A₂.RowBasis b₂
⊢ A₁.ColBasis t ↔ A₂.ColBasis tᶜ
Tactic:
rw [← orthSpace_rowSpace_eq_nullSpace, ← hb₁.rowSpace_eq, ← hb₂.rowSpace_eq] at h
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
⊢ A₁.ColBasis t ↔ A₂.ColBasis tᶜ
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
⊢ A₁.ColBasis t ↔ A₂.ColBasis tᶜ
Tactic:
rw [← hb₁.colBases_eq, ← hb₂.colBases_eq]
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
⊢ (A₁.rowSubmatrix b₁).ColBasis t ↔ (A₂.rowSubmatrix b₂).ColBasis tᶜ
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
⊢ (A₁.rowSubmatrix b₁).ColBasis t ↔ (A₂.rowSubmatrix b₂).ColBasis tᶜ
Tactic:
have _ := hb₁.finite.fintype
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝ : Fintype ↑b₁
⊢ (A₁.rowSubmatrix b₁).ColBasis t ↔ (A₂.rowSubmatrix b₂).ColBasis tᶜ
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝ : Fintype ↑b₁
⊢ (A₁.rowSubmatrix b₁).ColBasis t ↔ (A₂.rowSubmatrix b₂).ColBasis tᶜ
Tactic:
have _ := hb₂.finite.fintype
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
⊢ (A₁.rowSubmatrix b₁).ColBasis t ↔ (A₂.rowSubmatrix b₂).ColBasis tᶜ
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
⊢ (A₁.rowSubmatrix b₁).ColBasis t ↔ (A₂.rowSubmatrix b₂).ColBasis tᶜ
Tactic:
refine ⟨colBasis_iff_aux (by simp [h]) hb₁.linearIndependent hb₂.linearIndependent, fun h' ↦ ?_⟩
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
h' : (A₂.rowSubmatrix b₂).ColBasis tᶜ
⊢ (A₁.rowSubmatrix b₁).ColBasis t
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
h' : (A₂.rowSubmatrix b₂).ColBasis tᶜ
⊢ (A₁.rowSubmatrix b₁).ColBasis t
Tactic:
rw [← compl_compl t]
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
h' : (A₂.rowSubmatrix b₂).ColBasis tᶜ
⊢ (A₁.rowSubmatrix b₁).ColBasis tᶜᶜ
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
h' : (A₂.rowSubmatrix b₂).ColBasis tᶜ
⊢ (A₁.rowSubmatrix b₁).ColBasis tᶜᶜ
Tactic:
refine colBasis_iff_aux ?_ hb₂.linearIndependent hb₁.linearIndependent h'
Proof state after:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
h' : (A₂.rowSubmatrix b₂).ColBasis tᶜ
⊢ (A₂.rowSubmatrix b₂).rowSpace = (A₁.rowSubmatrix b₁).nullSpace
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
Proof state before:
case 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
K : Type u_14
inst✝³ : Field K
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
h' : (A₂.rowSubmatrix b₂).ColBasis tᶜ
⊢ (A₂.rowSubmatrix b₂).rowSpace = (A₁.rowSubmatrix b₁).nullSpace
Tactic:
rw [← orthSpace_rowSpace_eq_nullSpace, h, orthSpace_orthSpace]
Proof state after:
no goals
Theorem: Matrix.colBasis_iff_colBasis_compl_of_orth
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
inst✝² : Fintype n
m₁ : Type u_15
m₂ : Type u_16
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A : Matrix m n K
A₁ : Matrix m₁ n K
A₂ : Matrix m₂ n K
t : Set n
b₁ : Set m₁
hb₁ : A₁.RowBasis b₁
b₂ : Set m₂
h : (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).rowSpace.orthSpace
hb₂ : A₂.RowBasis b₂
x✝¹ : Fintype ↑b₁
x✝ : Fintype ↑b₂
⊢ (A₁.rowSubmatrix b₁).rowSpace = (A₂.rowSubmatrix b₂).nullSpace
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Matrix.rank'_eq_finrank_mulVecLin
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✝
R : Type u_14
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix m n R
⊢ A.rank' = finrank R ↥(LinearMap.range A.mulVecLin)
Tactic:
rw [rank', colSpace_eq_lin_range]
Proof state after:
no goals
Theorem: Matrix.ncard_colBasis
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
ht : A.ColBasis t
⊢ t.ncard = A.rank'
Tactic:
obtain (hfin | hinf) := t.finite_or_infinite
Proof state after:
case 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hfin : t.Finite
⊢ t.ncard = A.rank'

case 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hinf : t.Infinite
⊢ t.ncard = A.rank'
Theorem: Matrix.ncard_colBasis
Proof state before:
case 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hinf : t.Infinite
⊢ t.ncard = A.rank'
Tactic:
rw [hinf.ncard, rank', @finrank_of_infinite_dimensional _ _ _ _ _ fun hfin ↦ hinf <| ?_]
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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hinf : t.Infinite
hfin : FiniteDimensional K ↥A.colSpace
⊢ t.Finite
Theorem: Matrix.ncard_colBasis
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
ht : A.ColBasis t
hinf : t.Infinite
hfin : FiniteDimensional K ↥A.colSpace
⊢ t.Finite
Tactic:
have _ := ht.basis.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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hinf : t.Infinite
hfin : FiniteDimensional K ↥A.colSpace
x✝ : Finite ↑t
⊢ t.Finite
Theorem: Matrix.ncard_colBasis
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
ht : A.ColBasis t
hinf : t.Infinite
hfin : FiniteDimensional K ↥A.colSpace
x✝ : Finite ↑t
⊢ t.Finite
Tactic:
exact toFinite t
Proof state after:
no goals
Theorem: Matrix.ncard_colBasis
Proof state before:
case 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hfin : t.Finite
⊢ t.ncard = A.rank'
Tactic:
have _ := hfin.fintype
Proof state after:
case 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hfin : t.Finite
x✝ : Fintype ↑t
⊢ t.ncard = A.rank'
Theorem: Matrix.ncard_colBasis
Proof state before:
case 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
ht : A.ColBasis t
hfin : t.Finite
x✝ : Fintype ↑t
⊢ t.ncard = A.rank'
Tactic:
rw [rank', finrank, rank_eq_card_basis ht.basis, Cardinal.toNat_natCast,
  ← Nat.card_eq_fintype_card, Nat.card_coe_set_eq]
Proof state after:
no goals
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
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
hs : A.RowBasis s
ht : A.ColBasis t
⊢ s.ncard = t.ncard
Tactic:
have ht' := hs.submatrix_colBasis ht
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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
⊢ s.ncard = t.ncard
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
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
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
⊢ s.ncard = t.ncard
Tactic:
refine s.finite_or_infinite.elim (fun hfin ↦ ?_) (fun hinf ↦ ?_)
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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hfin : s.Finite
⊢ s.ncard = t.ncard

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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
⊢ s.ncard = t.ncard
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
⊢ s.ncard = t.ncard
Tactic:
rw [hinf.ncard, Infinite.ncard]
Proof 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
⊢ t.Infinite
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
⊢ t.Infinite
Tactic:
refine fun htfin ↦ hinf ?_
Proof 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
⊢ s.Finite
Theorem: Matrix.ncard_rowBasis_eq_ncard_colBasis
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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
⊢ s.Finite
Tactic:
have _ := htfin.fintype
Proof 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
K : Type u_14
inst✝ : Field K
A : Matrix m n K
hs : A.RowBasis s
ht : A.ColBasis t
ht' : (A.rowSubmatrix s).ColBasis t
hinf : s.Infinite
htfin : t.Finite
x✝ : Fintype ↑t
⊢ s.Finite