[GOAL]
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Finite ℤ M
hM : IsTorsion ℤ M
⊢ _root_.Finite M
[PROOFSTEP]
rcases Module.equiv_directSum_of_isTorsion hM with ⟨ι, _, p, h, e, ⟨l⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ _root_.Finite M
[PROOFSTEP]
haveI : ∀ i : ι, NeZero (p i ^ e i).natAbs := fun i => ⟨Int.natAbs_ne_zero.mpr <| pow_ne_zero (e i) (h i).ne_zero⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : 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 (Int.natAbs (p i ^ e i))
⊢ _root_.Finite M
[PROOFSTEP]
haveI : ∀ i : ι, _root_.Finite <| ℤ ⧸ Submodule.span ℤ {p i ^ e i} := fun i =>
  Finite.of_equiv _ (p i ^ e i).quotientSpanEquivZMod.symm.toEquiv
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : 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 (Int.natAbs (p i ^ e i))
this : ∀ (i : ι), _root_.Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ _root_.Finite M
[PROOFSTEP]
haveI : _root_.Finite (⨁ i, ℤ ⧸ (Submodule.span ℤ {p i ^ e i} : Submodule ℤ ℤ)) :=
  Finite.of_equiv _ DFinsupp.equivFunOnFintype.symm
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : 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 (Int.natAbs (p i ^ e i))
this✝ : ∀ (i : ι), _root_.Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
this : _root_.Finite (⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ _root_.Finite M
[PROOFSTEP]
exact Finite.of_equiv _ l.symm.toEquiv
[GOAL]
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
⊢ ∃ n ι x p x e, Nonempty (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ :=
  @Module.equiv_free_prod_directSum _ _ _ _ _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ ∃ n ι x p x e, Nonempty (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
refine' ⟨n, ι, fι, fun i => (p i).natAbs, fun i => _, e, ⟨_⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_1
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
i : ι
⊢ Nat.Prime ((fun i => Int.natAbs (p i)) i)
[PROOFSTEP]
rw [← Int.prime_iff_natAbs_prime, ← GCDMonoid.irreducible_iff_prime]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_1
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
i : ι
⊢ Irreducible (p i)
[PROOFSTEP]
exact hp i
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_2
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod ((fun i => Int.natAbs (p i)) i ^ e i)
[PROOFSTEP]
exact
  f.toAddEquiv.trans
    ((AddEquiv.refl _).prodCongr <|
      DFinsupp.mapRange.addEquiv fun i =>
        ((Int.quotientSpanEquivZMod _).trans <| ZMod.ringEquivCongr <| (p i).natAbs_pow _).toAddEquiv)
[GOAL]
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
cases' n with n
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.zero
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin Nat.zero →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
have : Unique (Fin Nat.zero →₀ ℤ) := { uniq := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton] }
[GOAL]
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin Nat.zero →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∀ (a : Fin Nat.zero →₀ ℤ), a = default
[PROOFSTEP]
simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.zero
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin Nat.zero →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Unique (Fin Nat.zero →₀ ℤ)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
exact ⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.succ
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (Nat.succ n) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
haveI := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.succ
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (Nat.succ n) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Fintype (Fin (Nat.succ n) →₀ ℤ)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
exact
  (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
      ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim
