l : Type ?u.158986
m : Type u_2
n : Type u_3
o : Type ?u.158995
R : Type u_1
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ finrank R { x // x ∈ Submodule.map (LinearMap.funLeft R R f) (LinearMap.range (mulVecLin A)) } ≤
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
l : Type ?u.158986
m : Type u_2
n : Type u_3
o : Type ?u.158995
R : Type u_1
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ rank (submatrix A f ↑e) ≤ rank A
rw [rank, rank, mulVecLin_submatrix, LinearMap.range_comp, LinearMap.range_comp,
  show LinearMap.funLeft R R e.symm = LinearEquiv.funCongrLeft R R e.symm from rfl,
  LinearEquiv.range, Submodule.map_top]
no goals
l : Type ?u.158986
m : Type u_2
n : Type u_3
o : Type ?u.158995
R : Type u_1
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
f : n → m
e : n ≃ m
A : Matrix m m R
⊢ finrank R { x // x ∈ Submodule.map (LinearMap.funLeft R R f) (LinearMap.range (mulVecLin A)) } ≤
    finrank R { x // x ∈ LinearMap.range (mulVecLin A) }
exact Submodule.finrank_map_le _ _