-- 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:
case mk.e_a
ι : 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'
⊢ ∏ x : { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ },
      (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
let f'' : Fin n ↪ { x // x ∈ Finset.filter (fun x ↦ ∃ j, f j = x) Finset.univ } :=
  ⟨f', hf'⟩

Result:
case mk.e_a
ι : 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 },
      (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Proof state:
case mk.e_a
ι : 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 },
      (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
have hu : (Finset.univ : Finset { x // x ∈ Finset.filter (fun x ↦ ∃ j, f j = x) Finset.univ }) =
  Finset.univ.map f'' := by
  ext x
  simp only [Finset.univ_eq_attach, Finset.mem_attach, Finset.mem_map, Finset.mem_univ,
    true_and, true_iff]
  have hx := x.property
  simp only [Finset.univ_filter_exists, Finset.mem_image, Finset.mem_univ, true_and] at hx
  rcases hx with ⟨i, hi⟩
  refine ⟨i, ?_⟩
  rw [Subtype.ext_iff]
  exact hi

Result:
case mk.e_a
ι : 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' }
hu : Finset.univ = Finset.map f'' Finset.univ
⊢ ∏ x : { x // x ∈ Finset.filter (fun x => ∃ j, f j = x) Finset.univ },
      (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Proof state:
case h.e'_3
ι : 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 : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ¬∃ j, f j = i
⊢ g i = 0

Tactic:
rw [← zero_dvd_iff]

Result:
case h.e'_3
ι : 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 : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ¬∃ j, f j = i
⊢ 0 ∣ g i

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)
i : Fin n
j : ι
⊢ (a i • Pi.single (f i) 1) j = Pi.single (f i) (a i) j

Tactic:
simp [Pi.single_apply]

Result:
no goals