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.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Free R N
inst✝ : Module.Finite R N
cond : finrank R M = finrank R N
⊢ Cardinal.lift (Module.rank R M) = Cardinal.lift (Module.rank R N)
simp only [← finrank_eq_rank, cond, lift_natCast]