theorem one_lt_rank_of_rank_lt_rank {𝕜 : Type u_1} [Field 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] {E' : Type u_3} [AddCommGroup E'] [Module 𝕜 E'] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'] {π : E →ₗ[𝕜] 𝕜} (hπ : LinearMap.ker π ≠ ⊤) (h : Module.finrank 𝕜 E < Module.finrank 𝕜 E') (φ : E →ₗ[𝕜] E') : 1 < Module.rank 𝕜 (E' ⧸ Submodule.map φ (LinearMap.ker π))