-- Mathlib/LinearAlgebra/FreeModule/Int.lean
/-- Given a submodule `N` in Smith normal form of a free `R`-module, its index as an additive
subgroup is an appropriate power of the cardinality of `R` multiplied by the product of the
indexes of the ideals generated by each basis vector. -/
lemma toAddSubgroup_index_eq_pow_mul_prod [Module R M] {N : Submodule R M}
    (snf : Basis.SmithNormalForm N ι n) :
    N.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) *
      ∏ i : Fin n, (Ideal.span {snf.a i}).toAddSubgroup.index

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN' : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
h : ∃ j, f j = i
⊢ (c h.choose * if i = f h.choose then a h.choose else 0) = c h.choose * a h.choose

Tactic:
simp [h.choose_spec]

Result:
no goals

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN'✝ : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i => Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ } := fun i => ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ } := { toFun := f', inj' := hf' }
x : { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ }
⊢ x ∈ Finset.univ ↔ x ∈ Finset.map f'' Finset.univ

Tactic:
simp only [Finset.univ_eq_attach, Finset.mem_attach, Finset.mem_map, Finset.mem_univ,
  true_and, true_iff]

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN'✝ : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i => Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ } := fun i => ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ } := { toFun := f', inj' := hf' }
x : { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ }
⊢ ∃ a, f'' a = x

Proof state:
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN' : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
h : ¬∃ j, f j = i
⊢ 0 ∣ ∑ x : Fin n, c x • if i = f x then a x else 0

Tactic:
convert dvd_refl (0 : R)

Result:
case h.e'_4
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN' : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
h : ¬∃ j, f j = i
⊢ (∑ x : Fin n, c x • if i = f x then a x else 0) = 0

Proof state:
case h.e'_3.h.e'_3.h
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN' : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
e : (ι → R) ≃+ M := ↑bM.equivFun.symm
he : e = ↑bM.equivFun.symm
e' : (ι → R) →+ M := ↑e
he' : Function.Surjective ⇑e'
e_2✝ : AddCommGroup.toAddGroup = Pi.addGroup
⊢ (Submodule.map bM.equivFun N).toAddSubgroup = AddSubgroup.map (↑↑bM.equivFun) N.toAddSubgroup

Tactic:
exact Submodule.map_toAddSubgroup ..

Result:
no goals

Proof state:
case h.refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN' : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∃ c, g = ∑ x : Fin n, c x • Pi.single (f x) (a x)
⊢ ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i

Tactic:
rcases h with ⟨c, rfl⟩

Result:
case h.refine_1.intro
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map bM.equivFun N
hN' : N' = Submodule.map bM.equivFun N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
⊢ ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ (∑ x : Fin n, c x • Pi.single (f x) (a x)) i