fapply FiniteDimensional.finrank_of_surjective_of_le_torsion
case h.e'_2.h.e'_6
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 ((M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N) = finrank R (M ⧸ N)

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
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
⊢ M ⧸ N →ₗ[R] (M ⧸ Submodule.torsion R M) ⧸ Submodule.map (Submodule.torsion R M).mkQ N

case h.e'_2.h.e'_6.hl
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
⊢ Function.Surjective ⇑?h.e'_2.h.e'_6.l

case h.e'_2.h.e'_6.hl'
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
⊢ LinearMap.ker ?h.e'_2.h.e'_6.l ≤ Submodule.torsion R (M ⧸ N)

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