-- Mathlib/LinearAlgebra/FreeModule/PID.lean
@[simp] lemma repr_apply_embedding_eq_repr_smul {i : Fin n} :
    snf.bM.repr m (snf.f i) = snf.bN.repr (snf.a i • m) i

Proof state:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t => t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩) (snf.f i) =
    (snf.bN.repr (snf.a i • ⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩)) i

Tactic:
simp_rw [hm, map_smul, map_finsupp_sum, 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]

Result:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t => t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩
⊢ c i = 0 → 0 = snf.a i * c i

Proof state:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t => t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩
⊢ c i = 0 → 0 = snf.a i * c i

Tactic:
exact fun a ↦ (mul_eq_zero_of_right _ a).symm

Result:
no goals

Proof state:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) (snf.f i) =
    (snf.bN.repr (snf.a i • ⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩)) i

Tactic:
replace hm : (⟨Finsupp.sum c fun i t ↦ t • (↑(snf.bN i) : M), hm⟩ : N) =
    Finsupp.sum c fun i t ↦ t • ⟨snf.bN i, (snf.bN i).2⟩ := by
  ext; change _ = N.subtype _; simp [map_finsupp_sum]

Result:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t => t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩) (snf.f i) =
    (snf.bN.repr (snf.a i • ⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩)) i

Proof state:
case mk
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
m : M
hm : m ∈ N
⊢ (snf.bM.repr ↑⟨m, hm⟩) (snf.f i) = (snf.bN.repr (snf.a i • ⟨m, hm⟩)) i

Tactic:
obtain ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm

Result:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) (snf.f i) =
    (snf.bN.repr (snf.a i • ⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩)) i

Proof state:
case mk.intro
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t => t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩
⊢ (snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩) (snf.f i) =
    (snf.bN.repr (snf.a i • ⟨c.sum fun i x => x • ↑(snf.bN i), hm✝⟩)) i

Tactic:
classical
simp_rw [hm, map_smul, map_finsupp_sum, 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

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ ⟨c.sum fun i t => t • ↑(snf.bN i), hm⟩ = c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩

Tactic:
ext

Result:
case a
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t => t • ↑(snf.bN i), hm⟩ = ↑(c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩)

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : Fin n
⊢ (snf.bM.repr ↑m) (snf.f i) = (snf.bN.repr (snf.a i • m)) i

Tactic:
obtain ⟨m, hm⟩ := m

Result:
case mk
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
m : M
hm : m ∈ N
⊢ (snf.bM.repr ↑⟨m, hm⟩) (snf.f i) = (snf.bN.repr (snf.a i • ⟨m, hm⟩)) i

Proof state:
case a
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t => t • ↑(snf.bN i), hm⟩ = N.subtype (c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩)

Tactic:
simp [map_finsupp_sum]

Result:
no goals

Proof state:
case a
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t => t • ↑(snf.bN i), hm⟩ = ↑(c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩)

Tactic:
change _ = N.subtype _

Result:
case a
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t => t • ↑(snf.bN i), hm⟩ = N.subtype (c.sum fun i t => t • ⟨↑(snf.bN i), ⋯⟩)