obtain ⟨s, hs, hs'⟩ := exists_finset_card_eq_finrank_and_linearIndependent R N
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M
case intro.intro
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
s : Finset ↥N
hs : s.card = finrank R ↥N
hs' : LinearIndependent R Subtype.val
⊢ finrank R ↥N + finrank R (M ⧸ N) ≤ finrank R M