rw [FiniteDimensional.finrank_quotient_of_le_torsion _ le_rfl,
  FiniteDimensional.finrank_map_of_le_torsion] at this
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
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R (M ⧸ Submodule.torsion 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
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥N + finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R M
⊢ finrank R ↥N + finrank R (M ⧸ N) = finrank R M

case hN
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
N : Submodule R M
this✝ : IsNoetherian R M
this :
  finrank R ↥(Submodule.map (Submodule.torsion R M).mkQ N) +
      finrank R ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) =
    finrank R M
⊢ N ⊓ LinearMap.ker (Submodule.torsion R M).mkQ ≤ Submodule.torsion R M