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
ι : Type w
p : ι → Submodule K V
hp : CompleteLattice.Independent p
inst✝ : Fintype { i // p i ≠ ⊥ }
⊢ Fintype.card { i // p i ≠ ⊥ } ≤ finrank K V
simpa using hp.subtype_ne_bot_le_finrank_aux