no goals
R : Type u
M : Type v
N : Type w
inst✝⁶ : Ring R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
s : Submodule R M
⊢ finrank R { x // x ∈ s } ≤ finrank R M
simpa only [Cardinal.toNat_lift] using
  toNat_le_of_le_of_lt_aleph0 (rank_lt_aleph0 _ _) (rank_submodule_le s)