-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm_1 : (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) ∈ N
hm :
  Subtype.mk (p := fun (x : M) ↦ x ∈ N)
      (c.sum fun (i : Fin n) (t : R) ↦ HSMul.hSMul (β := M) t (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) hm_1 =
    c.sum fun (i : Fin n) (t : R) ↦
      HSMul.hSMul (β := ↥N) t (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯)
simp_rw simp_rw₁ :
  Eq.{u_2 + 1} (α := R)
    (((snf.bM.repr : (a : M) → ι →₀ R)
            (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                  hm_1) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₂ :
  Eq.{u_2 + 1} (α := R)
    (((snf.bM.repr : (a : M) → ι →₀ R)
            (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (HSMul.hSMul (β := ↥N) (snf.a i)
                (c.sum fun (i : Fin n) (t : R) ↦
                  HSMul.hSMul (β := ↥N) t
                    (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯))) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((snf.bM.repr : (a : M) → ι →₀ R)
            (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M)) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((HSMul.hSMul (β := Fin n →₀ R) (snf.a i)
            ((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (c.sum fun (i : Fin n) (t : R) ↦
                HSMul.hSMul (β := ↥N) t
                  (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) i) : M) ⋯))) :
          (a : Fin n) → R)
        i :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((snf.bM.repr : (a : M) → ι →₀ R)
              (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                    (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                    hm_1) :
                M) :
            ι →₀ R) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (snf.a i •
                Subtype.mk (p := fun (x : M) ↦ x ∈ N)
                  (c.sum fun (i : Fin n) (x : R) ↦ HSMul.hSMul (β := M) x (↑((snf.bN : (a : Fin n) → ↥N) i) : M))
                  hm_1) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        i :
      R)
have simp_rw₄ : Eq.{u_2 + 1} (α := R)
  ((c.sum fun (a : Fin n) (b : R) ↦
          (snf.bM.repr : (a : M) → ι →₀ R) (HSMul.hSMul (β := M) b (↑((snf.bN : (a : Fin n) → ↥N) a) : M)) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) :
    R)
  ((HSMul.hSMul (β := Fin n →₀ R) (snf.a i)
          (c.sum fun (a : Fin n) (b : R) ↦
            (snf.bN.repr : (a : ↥N) → Fin n →₀ R)
              (HSMul.hSMul (β := ↥N) b
                (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) a) : M) sorry))) :
        (a : Fin n) → R)
      i :
    R)
Tactic: classical
  simp_rw [hm, map_smul, map_finsuppSum, map_smul, Subtype.coe_eta, repr_self,
    Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_single, Finsupp.smul_apply, snf.snf,
    map_smul, repr_self, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_apply,
    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Finsupp.sum_ite_eq',
    Finsupp.mem_support_iff, ite_not, mul_comm, ite_eq_right_iff]
  exact fun a ↦ (mul_eq_zero_of_right _ a).symm