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

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

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

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

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

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

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
x✝ : Fintype ↑t
⊢ s.Finite
Tactic:
have hs' := ht.submatrix_rowBasis hs
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
hs' : (A.colSubmatrix t).RowBasis s
⊢ s.Finite

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
x✝ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
⊢ s.Finite
Tactic:
have hb := hs'.basisFun ht.linearIndependent
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
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
⊢ s.Finite

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
x✝ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
⊢ s.Finite
Tactic:
have _ := hb.linearIndependent.fintype_index
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
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
x✝ : Fintype ↑s
⊢ s.Finite

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
x✝¹ : Fintype ↑t
hs' : (A.colSubmatrix t).RowBasis s
hb : Basis (↑s) K (↑t → K)
x✝ : Fintype ↑s
⊢ s.Finite
Tactic:
exact s.toFinite
State after:
no goals

State before:
case refine_1
l : Type u_1
m✝ : Type u_2
m' : Type u_3
n✝ : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R✝ : Type u_10
A✝¹ B✝ : Matrix m✝ n✝ R✝
s✝ : Set m✝
t✝ : Set n✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A✝ B : Matrix m n R
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
Tactic:
have _ := hfin.fintype
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
x✝ : Fintype ↑s
⊢ s.ncard = t.ncard

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
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
x✝ : Fintype ↑s
⊢ s.ncard = t.ncard
Tactic:
have hb := ht'.basisFun hs.linearIndependent
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
x✝ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
⊢ s.ncard = t.ncard

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
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
x✝ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
⊢ s.ncard = t.ncard
Tactic:
have _ := hb.linearIndependent.fintype_index
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
x✝¹ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
x✝ : Fintype ↑t
⊢ s.ncard = t.ncard

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
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
x✝¹ : Fintype ↑s
hb : Basis (↑t) K (↑s → K)
x✝ : Fintype ↑t
⊢ s.ncard = t.ncard
Tactic:
rw [← Nat.card_coe_set_eq, ← Nat.card_coe_set_eq, Nat.card_eq_fintype_card,
  Nat.card_eq_fintype_card, ← finrank_eq_card_basis hb, finrank_fintype_fun_eq_card]
State after:
no goals