Vector subspace of maximal dimension is top

Stream: Is there code for X?

[Stepan Nesterov]

Is the following theorem equivalent to a theorem in mathlib:

example {K : Type*} [Field K] (V : Type*) [AddCommGroup V] [Module K V] [Module.Finite K V]
  [Module.Free K V] (U : Submodule K V) (hUV : Module.rank K U = Module.rank K V) : U = ⊤ := by
  sorry

[Aaron Liu]

import Mathlib

example {K : Type*} [Field K] (V : Type*) [AddCommGroup V] [Module K V] [Module.Finite K V]
  [Module.Free K V] (U : Submodule K V) (hUV : Module.rank K U = Module.rank K V) : U = ⊤ := by
  apply Submodule.eq_of_le_of_finrank_eq le_top
  apply Module.finrank_eq_of_rank_eq
  rw [Module.finrank_eq_rank', hUV, rank_top]

[Kenny Lau]

https://loogle.lean-lang.org/ is an excellent tool to find lemmas. It contains instructions at the bottom.