no goals
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K { x // x ∈ S } = finrank K V
⊢ finrank K { x // x ∈ S } = finrank K { x // x ∈ ⊤ }
simp [h, finrank_top]