apply FiniteDimensional.finrank_quotient_of_le_torsion
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
M' : Type u_1
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
l : M →ₗ[R] M'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
⊢ finrank R (↥N ⧸ LinearMap.ker (l ∘ₗ N.subtype)) = finrank R ↥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
M' : Type u_1
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
l : M →ₗ[R] M'
inst✝ : Module.Finite R ↥N
hN : N ⊓ LinearMap.ker l ≤ Submodule.torsion R M
⊢ LinearMap.ker (l ∘ₗ N.subtype) ≤ Submodule.torsion R ↥N