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₂
s : Submodule K V
lt : finrank K { x // x ∈ s } < finrank K { x // x ∈ ⊤ }
⊢ s < ⊤
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₂
s : Submodule K V
lt : finrank K { x // x ∈ s } < finrank K V
⊢ s < ⊤
rw [← finrank_top K V] at lt
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₂
s : Submodule K V
lt : finrank K { x // x ∈ s } < finrank K { x // x ∈ ⊤ }
⊢ s < ⊤
exact lt_of_le_of_finrank_lt_finrank le_top lt