have _ := hb.linearIndependent.fintype_index
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
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