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
case h
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
l : ↑(Set.range ⇑B.snd.f)ᶜ →₀ R
hl : ∑ i : ↑(Set.range ⇑B.snd.f)ᶜ, l i • (⇑B.snd.bM ∘ Subtype.val) i ∈ N
i : ↑(Set.range ⇑B.snd.f)ᶜ
⊢ l i = 0 i
no goals