rw [← hb₁.colBases_eq, ← hb₂.colBases_eq]
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ᶜ
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ᶜ