-- 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 infinite (represented as zero) if the submodule basis has fewer vectors than the basis
for the module, and otherwise equals the product of the indexes of the ideals generated by each
basis vector. -/
lemma toAddSubgroup_index_eq_ite [Infinite R] [Module R M] {N : Submodule R M}
    (snf : Basis.SmithNormalForm N ι n) : N.toAddSubgroup.index = (if n = Fintype.card ι then
      ∏ i : Fin n, (Ideal.span {snf.a i}).toAddSubgroup.index else 0)

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✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index = 0

Tactic:
have hlt : n < Fintype.card ι :=
  Ne.lt_of_le h (by simpa using Fintype.card_le_of_embedding snf.f)

Result:
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
hlt : n < Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index = 0

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✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
hlt : n < Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index = 0

Tactic:
simp [hlt]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index =
    if n = Fintype.card ι then ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index =
    ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index

case neg
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index = 0

Proof state:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : n = Fintype.card ι
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index =
    ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ N.toAddSubgroup.index =
    if n = Fintype.card ι then ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0

Tactic:
rw [snf.toAddSubgroup_index_eq_pow_mul_prod]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ Nat.card R ^ (Fintype.card ι - n) * ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index =
    if n = Fintype.card ι then ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
h : ¬n = Fintype.card ι
⊢ n ≤ Fintype.card ι

Tactic:
simpa using Fintype.card_le_of_embedding snf.f

Result:
no goals