-- Mathlib/GroupTheory/FiniteAbelian/Basic.lean
theorem finite_of_fg_torsion [AddCommGroup M] [Module ℤ M] [Module.Finite ℤ M]
    (hM : Module.IsTorsion ℤ M) : _root_.Finite M

Proof state:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this✝ : ∀ (i : ι), NeZero (p i ^ e i).natAbs
this : ∀ (i : ι), Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ Finite M

Tactic:
haveI : _root_.Finite (⨁ i, ℤ ⧸ (Submodule.span ℤ {p i ^ e i} : Submodule ℤ ℤ)) :=
  Finite.of_equiv _ DFinsupp.equivFunOnFintype.symm

Result:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this✝¹ : ∀ (i : ι), NeZero (p i ^ e i).natAbs
this✝ : ∀ (i : ι), Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
this : Finite (⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ Finite M

Proof state:
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
⊢ Finite M

Tactic:
rcases Module.equiv_directSum_of_isTorsion hM with ⟨ι, _, p, h, e, ⟨l⟩⟩

Result:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ Finite M

Proof state:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this : ∀ (i : ι), NeZero (p i ^ e i).natAbs
⊢ Finite M

Tactic:
haveI : ∀ i : ι, _root_.Finite <| ℤ ⧸ Submodule.span ℤ {p i ^ e i} := fun i =>
  Finite.of_equiv _ (p i ^ e i).quotientSpanEquivZMod.symm.toEquiv

Result:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this✝ : ∀ (i : ι), NeZero (p i ^ e i).natAbs
this : ∀ (i : ι), Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ Finite M

Proof state:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this✝¹ : ∀ (i : ι), NeZero (p i ^ e i).natAbs
this✝ : ∀ (i : ι), Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
this : Finite (⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ Finite M

Tactic:
exact Finite.of_equiv _ l.symm.toEquiv

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ Finite M

Tactic:
haveI : ∀ i : ι, NeZero (p i ^ e i).natAbs := fun i =>
  ⟨Int.natAbs_ne_zero.mpr <| pow_ne_zero (e i) (h i).ne_zero⟩

Result:
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this : ∀ (i : ι), NeZero (p i ^ e i).natAbs
⊢ Finite M