-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
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
g : ι → R
h :
  ∀ (i : ι),
    (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) ∣
      g i
i : ι
hj : ∃ (j : Fin n), (f : (a : Fin n) → ι) j = i
h₁ :
  i = (f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) →
    ∀ (x : R),
      (if h :
            ∃ (j : Fin n),
              Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
                ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι) then
          a
            (h.choose (p := fun (j : Fin n) ↦
              Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
                ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι)))
        else 0) =
        a (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
convert_3 :
  ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ b →
      b ≠ hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i) →
        (if i = (f : (a : Fin n) → ι) b then
            Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) b) = a b * c) ⋯ • a b
          else 0) =
          0
⊢ (∑ x : Fin n,
      if i = (f : (a : Fin n) → ι) x then
        Exists.choose (p := fun (c : R) ↦ g ((f : (a : Fin n) → ι) x) = a x * c) ⋯ • a x
      else 0) =
    if i = (f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) then
      Exists.choose (p := fun (c : R) ↦
          g ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))) =
            (if h :
                  ∃ (j : Fin n),
                    Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
                      ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι) then
                a
                  (h.choose (p := fun (j : Fin n) ↦
                    Eq (α := ι) ((f : (a : Fin n) → ι) j : ι)
                      ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) : ι)))
              else 0) *
              c)
          ⋯ *
        a (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
    else 0
have convert_4 : hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i) ∉ Finset.univ →
  (if i = (f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) then
      Exists.choose (p := fun (c : R) ↦
          g ((f : (a : Fin n) → ι) (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))) =
            a (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i)) * c)
          sorry •
        a (hj.choose (p := fun (j : Fin n) ↦ (f : (a : Fin n) → ι) j = i))
    else 0) =
    0
Tactic: convert! Finset.sum_eq_single (M := R) hj.choose ?_ ?_