simp [ColBasis, rowBasis_iff_maximal_linearIndependent, rowFun_rowSubmatrix_eq,
  colFun_colSubmatrix_eq]
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}
no goals