-- Mathlib/LinearAlgebra/FreeModule/Int.lean
/-- Given a submodule `N` in Smith normal form of a free ℤ-module, it has finite index as an
additive subgroup (i.e., `N.toAddSubgroup.index ≠ 0`) if and only if the submodule basis has as
many vectors as the basis for the module. -/
lemma toAddSubgroup_index_ne_zero_iff {N : Submodule ℤ M} (snf : Basis.SmithNormalForm N ι n) :
    N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι

Proof state:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
i : Fin n
hi : a i = 0
snf : ↑(bN i) = a i • bM (f i)
⊢ bN i = 0

Tactic:
simpa [hi] using snf

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
i : Fin n
hi : a i = 0
⊢ bN i = 0

Tactic:
specialize snf i

Result:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
i : Fin n
hi : a i = 0
snf : ↑(bN i) = a i • bM (f i)
⊢ bN i = 0

Proof state:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ n = Fintype.card ι → ¬∏ x : Fin n, (Submodule.toAddSubgroup (Ideal.span {a x})).index = 0

Tactic:
have ha : ∀ i, a i ≠ 0 := by
  intro i hi
  apply Basis.ne_zero bN i
  specialize snf i
  simpa [hi] using snf

Result:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
ha : ∀ (i : Fin n), a i ≠ 0
⊢ n = Fintype.card ι → ¬∏ x : Fin n, (Submodule.toAddSubgroup (Ideal.span {a x})).index = 0

Proof state:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
i : Fin n
hi : a i = 0
⊢ False

Tactic:
apply Basis.ne_zero bN i

Result:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
i : Fin n
hi : a i = 0
⊢ bN i = 0

Proof state:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
ha : ∀ (i : Fin n), a i ≠ 0
⊢ n = Fintype.card ι → ¬∏ x : Fin n, (Submodule.toAddSubgroup (Ideal.span {a x})).index = 0

Tactic:
intro h

Result:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
ha : ∀ (i : Fin n), a i ≠ 0
h : n = Fintype.card ι
⊢ ¬∏ x : Fin n, (Submodule.toAddSubgroup (Ideal.span {a x})).index = 0

Proof state:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ (if n = Fintype.card ι then
        ∏ i : Fin n,
          (Submodule.toAddSubgroup (Ideal.span {{ bM := bM, bN := bN, f := f, a := a, snf := snf }.a i})).index
      else 0) ≠
      0 ↔
    n = Fintype.card ι

Tactic:
simp only [ne_eq, ite_eq_right_iff, Classical.not_imp, and_iff_left_iff_imp]

Result:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ n = Fintype.card ι → ¬∏ x : Fin n, (Submodule.toAddSubgroup (Ideal.span {a x})).index = 0

Proof state:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ (if n = Fintype.card ι then ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0) ≠ 0 ↔
    n = Fintype.card ι

Tactic:
rcases snf with ⟨bM, bN, f, a, snf⟩

Result:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ (if n = Fintype.card ι then
        ∏ i : Fin n,
          (Submodule.toAddSubgroup (Ideal.span {{ bM := bM, bN := bN, f := f, a := a, snf := snf }.a i})).index
      else 0) ≠
      0 ↔
    n = Fintype.card ι

Proof state:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ ∀ (i : Fin n), a i ≠ 0

Tactic:
intro i hi

Result:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
i : Fin n
hi : a i = 0
⊢ False

Proof state:
case mk
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
ha : ∀ (i : Fin n), a i ≠ 0
h : n = Fintype.card ι
⊢ ¬∏ x : Fin n, (Submodule.toAddSubgroup (Ideal.span {a x})).index = 0

Tactic:
simpa [Ideal.span_singleton_toAddSubgroup_eq_zmultiples, Int.index_zmultiples,
  Finset.prod_eq_zero_iff] using ha

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι

Tactic:
rw [snf.toAddSubgroup_index_eq_ite]

Result:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ (if n = Fintype.card ι then ∏ i : Fin n, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0) ≠ 0 ↔
    n = Fintype.card ι