rfl
case h.e'_3.h.e'_6.h
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
x : n → R
⊢ (∃ a, ↑(b a) = x) ↔ ∃ y, (Matrix.of fun i j => ↑(b i) j).rowFun y = x
no goals