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✝³ : Module.Finite R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
⊢ ↑(finrank R M) = Module.rank R M
rw [finrank, cast_toNat_of_lt_aleph0 (rank_lt_aleph0 R M)]