no goals
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : Injective ↑f
⊢ finrank K { x // x ∈ range f } = finrank K V
rw [(LinearEquiv.ofInjective f hf).finrank_eq]