rw [rowFun_rowSubmatrix_eq, range_restrict]
case intro.intro.intro.intro.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
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ range (A.rowSubmatrix s).rowFun ⊆ range A.rowFun
case intro.intro.intro.intro.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
inst✝ : DivisionRing R
A : Matrix m n R
s₀ : Set m
hs₀ : LinearIndependent (ι := ↑s₀) R (A.rowSubmatrix s₀).rowFun
s : Set m
hss : s₀ ⊆ s
h1 : A '' univ ⊆ ↑(span R (A '' s))
h2 : LinearIndependent (ι := ↑s) R (s.restrict A)
⊢ A.rowFun '' s ⊆ range A.rowFun