simp
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 : (l.sum fun i a => a • (⇑B.snd.bM ∘ Subtype.val) i) ∈ N
i : ↑(Set.range ⇑B.snd.f)ᶜ
⊢ ∀ (i : ↑(Set.range ⇑B.snd.f)ᶜ), 0 • (⇑B.snd.bM ∘ Subtype.val) i = 0
no goals