have : LinearIndependent R (N.mkQ ∘ B.2.bM ∘ Subtype.val : ((Set.range B.2.f)ᶜ : _) → _) := by
  rw [linearIndependent_iff]
  intros l hl
  ext i
  rw [← Finsupp.apply_total, N.mkQ_apply, Submodule.Quotient.mk_eq_zero, Finsupp.total_apply,
    Finsupp.sum_fintype _ _ (by simp)] at hl
  simpa only [Function.comp_apply, map_sum, map_smul, Basis.repr_self, Finsupp.smul_single,
    smul_eq_mul, mul_one, Finsupp.single_apply, Finsupp.finset_sum_apply,
    ← Subtype.ext_iff, Finset.sum_ite_eq', Finset.mem_univ, ite_true] using
    B.2.repr_eq_zero_of_nmem_range ⟨_, hl⟩ i.prop
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)
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
inst✝ : Module.Free R M
N : Submodule R M
B : (n : ℕ) × Basis.SmithNormalForm N (Module.Free.ChooseBasisIndex R M) n :=
  Submodule.smithNormalForm (Module.Free.chooseBasis R M) N
this : LinearIndependent (ι := ↑(Set.range ⇑B.snd.f)ᶜ) R (⇑N.mkQ ∘ ⇑B.snd.bM ∘ Subtype.val)
⊢ finrank R M - finrank R ↥N ≤ finrank R (M ⧸ N)