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₂
h : lift (Module.rank K V) ≤ lift (Module.rank K V₂)
h' : Module.rank K V₂ < ℵ₀
⊢ finrank K V ≤ finrank K V₂
simpa only [toNat_lift] using toNat_le_of_le_of_lt_aleph0 (lift_lt_aleph0.mpr h') h