rw [← LinearMap.finrank_range_of_inj (LinearMap.domRestrict_injective hf _),
  LinearMap.range_domRestrict]
K : Type u_1
V : Type u_2
V₂ : Type u_3
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : Function.Injective ⇑f
U : Submodule K V
⊢ FiniteDimensional.finrank K ↥(Submodule.map f U) = FiniteDimensional.finrank K ↥U
no goals