apply (finrank_add_finrank_quotient_le N).antisymm
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
N✝ : Submodule R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Module.Free R M
N : Submodule R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
N✝ : Submodule R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Module.Free R M
N : Submodule R M
⊢ finrank R M ≤ finrank R ↥N + finrank R (M ⧸ N)