-- Module: Mathlib.LinearAlgebra.FreeModule.Int
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Fintype ι
inst_3 : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis.{0, u_2, u_3} (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
hN' : N' = Submodule.map (↑bM.equivFun : M →ₗ[R] ι → R) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' :
  ∀ (i : Fin n),
    Eq (α := ι → R) ((↑((bN' : (a : Fin n) → ↥N') i) : ι → R) : ι → R)
      (Pi.single (M := fun (j : ι) ↦ R) ((f : (a : Fin n) → ι) i) (a i) : (j : ι) → R)
hNN' : N.toAddSubgroup.index = AddSubgroup.index (G := ι → R) N'.toAddSubgroup
⊢ Eq (α := AddSubgroup (ι → R)) N'.toAddSubgroup
    (AddSubgroup.pi (f := fun (i : ι) ↦ R) Set.univ fun (i : ι) ↦
      Submodule.toAddSubgroup
        (Ideal.span
          {if h : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i then
              a (h.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
            else 0}))

Tactic:
have hN' : N'.toAddSubgroup = AddSubgroup.pi Set.univ
      (fun i ↦ (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0}).toAddSubgroup) := by
    ext g
    simp only [Submodule.mem_toAddSubgroup, bN'.mem_submodule_iff', snf', AddSubgroup.mem_pi,
      Set.mem_univ, true_implies, Ideal.mem_span_singleton]
    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · rcases h with ⟨c, rfl⟩
      intro i
      simp only [Finset.sum_apply, Pi.smul_apply, Pi.single_apply]
      split_ifs with h
      · convert! dvd_mul_left (a h.choose) (c h.choose)
        calc ∑ x : Fin n, _ = c h.choose * if i = f h.choose then a h.choose else 0 := by
              refine Finset.sum_eq_single h.choose ?_ (by simp)
              rintro j - hj
              have hinj := f.injective.ne hj
              rw [h.choose_spec] at hinj
              simp [hinj.symm]
          _ = c h.choose * a h.choose := by simp [h.choose_spec]
      · convert! dvd_refl (0 : R)
        convert! Finset.sum_const_zero with j
        rw [not_exists] at h
        specialize h j
        rw [eq_comm] at h
        simp [h]
    · refine ⟨fun j ↦ (h (f j)).choose, ?_⟩
      ext i
      simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq,
        Finset.sum_apply, Pi.smul_apply, Pi.single_apply, smul_ite, smul_zero]
      rw [eq_comm]
      by_cases! hj : ∃ j, f j = i
      · calc ∑ x : Fin n, _ =
            if i = f hj.choose then (h (f hj.choose)).choose * a hj.choose else 0 := by
              convert! Finset.sum_eq_single (M := R) hj.choose ?_ ?_
              · simp
              · rintro j - h
                have hinj := f.injective.ne h
                rw [hj.choose_spec] at hinj
                simp [hinj.symm]
              · simp
          _ = g i := by
              simp only [hj.choose_spec, ↓reduceIte]
              rw [mul_comm]
              conv_rhs =>
                rw [← hj.choose_spec, (h (f hj.choose)).choose_spec]
              simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq]
              congr!
              · exact hj.choose_spec.symm
              · simp [hj]
      · convert! Finset.sum_const_zero with x
        · specialize hj x
          rw [ne_comm] at hj
          simp [hj]
        · rw [← zero_dvd_iff]
          convert! h i
          simp [hj]