rw [Matrix.rowSpace, map_span]
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ b.toRowMatrix.rowSpace = map U.subtype (span R (range ⇑b))
case h.e'_2
R : Type u_1
m : Type u_2
n : Type u_3
inst✝ : CommRing R
U : Submodule R (n → R)
b : Basis m R ↥U
⊢ span R (range b.toRowMatrix.rowFun) = span R (⇑U.subtype '' range ⇑b)