-- 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)
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) ⋯))) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₅ :
  Eq.{u_2 + 1} (α := R)
    ((c.sum fun (a : Fin n) (b : R) ↦
            HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((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) ↦
              HSMul.hSMul (β := Fin n →₀ R) b
                ((snf.bN.repr : (a : ↥N) → Fin n →₀ R)
                    (Subtype.mk (p := fun (x : M) ↦ x ∈ N) (↑((snf.bN : (a : Fin n) → ↥N) a) : M) ⋯) :
                  Fin n →₀ R)) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₆ :
  Eq.{u_2 + 1} (α := R)
    ((c.sum fun (a : Fin n) (b : R) ↦
            HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((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) ↦
              HSMul.hSMul (β := Fin n →₀ R) b
                ((snf.bN.repr : (a : ↥N) → Fin n →₀ R) ((snf.bN : (a : Fin n) → ↥N) a) : Fin n →₀ R)) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₇ :
  Eq.{u_2 + 1} (α := R)
    ((c.sum fun (a : Fin n) (b : R) ↦
            HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((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) ↦ HSMul.hSMul (β := Fin n →₀ R) b (Finsupp.single a 1)) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₈ :
  Eq.{u_2 + 1} (α := R)
    ((c.sum fun (a : Fin n) (b : R) ↦
            HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((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) ↦ Finsupp.single a (HSMul.hSMul (β := R) b 1)) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₉ :
  Eq.{u_2 + 1} (α := R)
    ((c.sum fun (a : Fin n) (b : R) ↦
            HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((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) ↦ Finsupp.single a (b * 1)) :
          (a : Fin n) → R)
        i :
      R)
simp_rw₁₀ :
  Eq.{u_2 + 1} (α := R)
    ((c.sum fun (a : Fin n) (b : R) ↦
            HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((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) ↦ Finsupp.single a b) : (a : Fin n) → R)
        i :
      R)
simp_rw₁₁ :
  Eq.{u_2 + 1} (α := R)
    ((c.sum fun (a : Fin n) (b : R) ↦
            HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((snf.bN : (a : Fin n) → ↥N) a) : M)) :
          (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι) :
      R)
    ((snf.a i • c : (a : Fin n) → R) i : R)
simp_rw₁₂ :
  (c.sum fun (a : Fin n) (b : R) ↦
          HSMul.hSMul (β := ι →₀ R) b ((snf.bM.repr : (a : M) → ι →₀ R) (↑((snf.bN : (a : Fin n) → ↥N) a) : M)) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) =
    HSMul.hSMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₁₃ :
  (c.sum fun (a : Fin n) (b : R) ↦
          HSMul.hSMul (β := ι →₀ R) b
            ((snf.bM.repr : (a : M) → ι →₀ R)
                (HSMul.hSMul (β := M) (snf.a a) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) a : ι) : M)) :
              ι →₀ R) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) =
    HSMul.hSMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₁₄ :
  (c.sum fun (a : Fin n) (b : R) ↦
          b •
            HSMul.hSMul (β := ι →₀ R) (snf.a a)
              ((snf.bM.repr : (a : M) → ι →₀ R) ((snf.bM : (a : ι) → M) ((snf.f : (a : Fin n) → ι) a : ι)) : ι →₀ R) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) =
    HSMul.hSMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₁₅ :
  (c.sum fun (a : Fin n) (b : R) ↦
          b • HSMul.hSMul (β := ι →₀ R) (snf.a a) (Finsupp.single ((snf.f : (a : Fin n) → ι) a) 1 : ι →₀ R) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) =
    HSMul.hSMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₁₆ :
  (c.sum fun (a : Fin n) (b : R) ↦ Finsupp.single ((snf.f : (a : Fin n) → ι) a) (b • HSMul.hSMul (β := R) (snf.a a) 1) :
        (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) =
    HSMul.hSMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₁₇ :
  (c.sum fun (a : Fin n) (b : R) ↦ Finsupp.single ((snf.f : (a : Fin n) → ι) a) (b * (snf.a a * 1)) : (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) =
    HMul.hMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₁₈ :
  (c.sum fun (a : Fin n) (b : R) ↦ Finsupp.single ((snf.f : (a : Fin n) → ι) a) (b * snf.a a) : (a : ι) → R)
      ((snf.f : (a : Fin n) → ι) i : ι) =
    HMul.hMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₁₉ :
  (c.sum fun (a₁ : Fin n) (b : R) ↦
      ((Finsupp.single ((snf.f : (a : Fin n) → ι) a₁) (b * snf.a a₁) : ι →₀ R) : (a : ι) → R)
        ((snf.f : (a : Fin n) → ι) i : ι)) =
    HMul.hMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₂₀ :
  (c.sum fun (a₁ : Fin n) (b : R) ↦
      if Eq (α := ι) ((snf.f : (a : Fin n) → ι) a₁ : ι) ((snf.f : (a : Fin n) → ι) i : ι) then b * snf.a a₁ else 0) =
    HMul.hMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₂₁ :
  (c.sum fun (a₁ : Fin n) (b : R) ↦ if a₁ = i then b * snf.a a₁ else 0) =
    HMul.hMul (β := R) (snf.a i) ((c : (a : Fin n) → R) i : R)
simp_rw₂₂ :
  (if i ∈ c.support then HMul.hMul (α := R) ((c : (a : Fin n) → R) i : R) (snf.a i) else 0) =
    HMul.hMul (β := R) (snf.a i) ((c : (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₂₃ : (if Ne (α := R) ((c : (a : Fin n) → R) i : R) (0 : R) then HMul.hMul (α := R) ((c : (a : Fin n) → R) i : R) (snf.a i)
  else 0) =
  HMul.hMul (β := R) (snf.a i) ((c : (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