rw [LinearMap.ker_comp, ← Submodule.map_le_iff_le_comap, Submodule.ker_mkQ]
case h.e'_2.h.e'_6.l
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
⊢ N ≤ LinearMap.ker ((Submodule.map (Submodule.torsion R M).mkQ N).mkQ ∘ₗ (Submodule.torsion R M).mkQ)
no goals