-- Mathlib/LinearAlgebra/FreeModule/Int.lean
lemma submodule_toAddSubgroup_index_ne_zero_iff {N : Submodule ℤ (ι → ℤ)} :
    N.toAddSubgroup.index ≠ 0 ↔ Nonempty (N ≃ₗ[ℤ] (ι → ℤ))

Proof state:
case mk.mk.refine_1
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
this : Fintype ι
bN : Basis (Fin (Fintype.card ι)) ℤ ↥N
⊢ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
exact ⟨(bN.reindex (Fintype.equivFin _).symm).equivFun⟩

Result:
no goals

Proof state:
case mk.mk.refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
⊢ n = Fintype.card ι

Tactic:
have hc := card_eq_of_linearEquiv ℤ <| bN.equivFun.symm.trans e

Result:
case mk.mk.refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
hc : Fintype.card (Fin n) = Fintype.card ι
⊢ n = Fintype.card ι

Proof state:
case mk.mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ ?_⟩

Result:
case mk.mk.refine_1
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
h : n = Fintype.card ι
⊢ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

case mk.mk.refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
⊢ n = Fintype.card ι

Proof state:
case mk.mk.refine_1
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
h : n = Fintype.card ι
⊢ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
subst h

Result:
case mk.mk.refine_1
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
this : Fintype ι
bN : Basis (Fin (Fintype.card ι)) ℤ ↥N
⊢ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Proof state:
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
obtain ⟨n, snf⟩ := N.smithNormalForm <| Basis.ofEquivFun <| LinearEquiv.refl _ _

Result:
case mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Basis.SmithNormalForm N ι n
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Proof state:
case mk.mk.refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
hc : Fintype.card (Fin n) = Fintype.card ι
⊢ n = Fintype.card ι

Tactic:
simpa using hc

Result:
no goals

Proof state:
case mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
rw [snf.toAddSubgroup_index_ne_zero_iff]

Result:
case mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Proof state:
case mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
rcases snf with ⟨-, bN, -, -, -⟩

Result:
case mk.mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Basis (Fin n) ℤ ↥N
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Proof state:
case mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Basis.SmithNormalForm N ι n
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
have := Fintype.ofFinite ι

Result:
case mk
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)