awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
M : Type u
inst : AddCommGroup M
inst_1 : Module ℤ M
inst_2 : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
⊢ ∀ (i : ι), NeZero (p i ^ e i).natAbs

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⟩
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
M : Type u
inst : AddCommGroup M
inst_1 : Module ℤ M
inst_2 : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
this : ∀ (i : ι), NeZero (p i ^ e i).natAbs
⊢ ∀ (i : ι), Finite (HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i))

Tactic:
haveI : ∀ i : ι, _root_.Finite <| ℤ ⧸ Submodule.span ℤ {p i ^ e i} := fun i =>
    Finite.of_equiv _ (p i ^ e i).quotientSpanEquivZMod.symm.toEquiv
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
M : Type u
inst : AddCommGroup M
inst_1 : Module ℤ M
inst_2 : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
this_1 : ∀ (i : ι), NeZero (p i ^ e i).natAbs
this : ∀ (i : ι), Finite (HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i))
⊢ Finite (⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i))

Tactic:
haveI : _root_.Finite (⨁ i, ℤ ⧸ (Submodule.span ℤ {p i ^ e i} : Submodule ℤ ℤ)) :=
    Finite.of_equiv _ DFinsupp.equivFunOnFintype.symm
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
M : Type u
inst : AddCommGroup M
inst_1 : Module ℤ M
inst_2 : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
this_1 : ∀ (i : ι), NeZero (p i ^ e i).natAbs
this_2 : ∀ (i : ι), Finite (HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i))
this : Finite (⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i))
⊢ Finite M

Tactic:
Finite.of_equiv _ l.symm.toEquiv

Premises used: Finite.of_equiv, LinearEquiv.symm, LinearEquiv.toEquiv
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
M : Type u
inst : AddCommGroup M
inst_1 : Module ℤ M
inst_2 : Module.Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
this_1 : ∀ (i : ι), NeZero (p i ^ e i).natAbs
this_2 : ∀ (i : ι), Finite (HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i))
this : Finite (⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i))
⊢ Finite M

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

Premises used: Finite.of_equiv, LinearEquiv.symm, LinearEquiv.toEquiv
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
hG : AddGroup.FG G
obtain :
  ∀ (n : ℕ) (ι : Type) (fι : Fintype ι) (p : ι → ℤ) (hp : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ)
    (f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)),
    ∃ (n : ℕ) (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u + 1)} (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
⊢ ∃ (n : ℕ) (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ :=
    @Module.equiv_free_prod_directSum _ _ _ _ _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG)

Premises used: Module.equiv_free_prod_directSum
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
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 : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
⊢ ∃ (n : ℕ) (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
⟨n, ι, fι, fun i => (p i).natAbs, fun i => ?_, e, ⟨?_⟩⟩

Premises used: Nonempty.intro, Int.natAbs, Exists.intro
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
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 : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
refine_1 : ∀ (i : ι), Nat.Prime ((fun (i : ι) ↦ (p i).natAbs) i)
refine_2 : G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (HPow.hPow (α := ℕ) ((fun (i : ι) ↦ (p i).natAbs) i) (e i))
⊢ ∃ (n : ℕ) (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
refine ⟨n, ι, fι, fun i => (p i).natAbs, fun i => ?_, e, ⟨?_⟩⟩
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
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 : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
i : ι
refine_1 : Irreducible (p i)
⊢ Nat.Prime ((fun (i : ι) ↦ (p i).natAbs) i)

Tactic:
rw [← Int.prime_iff_natAbs_prime, ← irreducible_iff_prime]

Premises used: Int.prime_iff_natAbs_prime, irreducible_iff_prime
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
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 : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
i : ι
⊢ Irreducible (p i)

Tactic:
hp i
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
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 : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
i : ι
⊢ Irreducible (p i)

Tactic:
exact hp i
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
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 : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)
⊢ G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (HPow.hPow (α := ℕ) ((fun (i : ι) ↦ (p i).natAbs) i) (e i))

Tactic:
exact
    f.toAddEquiv.trans
      ((AddEquiv.refl _).prodCongr <|
        DFinsupp.mapRange.addEquiv fun i =>
          ((Int.quotientSpanEquivZMod _).trans <|
              ZMod.ringEquivCongr <| (p i).natAbs_pow _).toAddEquiv)

Premises used: ZMod.ringEquivCongr, RingEquiv.toAddEquiv, LinearEquiv.toAddEquiv, Int.quotientSpanEquivZMod, Int.natAbs_pow, AddEquiv.prodCongr, HPow.hPow, AddEquiv.trans, AddEquiv.refl, RingEquiv.trans, DFinsupp.mapRange.addEquiv
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
intro :
  ∀ (val : Fintype G),
    ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
cases nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
intro :
  ∀ (n : ℕ) (ι : Type) (fι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ)
    (f : G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)),
    ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G

Premises used: AddCommGroup.equiv_free_prod_directSum_zmod
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : 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)
intro :
  ∀ (f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)),
    ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
intro₁ :
  ∀ (n : ℕ) (f : G ≃+ (Fin (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)),
    ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
rcases n with - | n
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∀ (a : Fin Nat.zero →₀ ℤ), a = default

Tactic:
subsingleton
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
intro :
  ∀ (this : Unique (Fin Nat.zero →₀ ℤ)),
    ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
have : Unique (Fin Nat.zero →₀ ℤ) :=
      { uniq := by subsingleton }
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Unique (Fin Nat.zero →₀ ℤ)
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩

Premises used: AddEquiv.uniqueProd, Nonempty.intro, AddEquiv.trans, Exists.intro
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Unique (Fin Nat.zero →₀ ℤ)
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
exact ⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
intro :
  ∀ (this : Fintype (Fin (n + 1) →₀ ℤ)),
    ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
haveI := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Fintype (Fin (n + 1) →₀ ℤ)
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
(Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
            ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim

Premises used: Finsupp.single_eq_same, False.elim, Fintype.ofSurjective, Fintype.false, Exists.intro, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
val : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Fintype (Fin (n + 1) →₀ ℤ)
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
exact
      (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
            ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim

Premises used: Finsupp.single_eq_same, False.elim, Fintype.ofSurjective, Fintype.false, Exists.intro, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
obtain :
  ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
    (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)),
    ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
      (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G

Premises used: AddCommGroup.equiv_directSum_zmod_of_finite
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩

Premises used: inferInstance, Subtype, Ne, Nonempty.intro, HPow.hPow, AddEquiv.trans, And.intro, Exists.intro, OfNat.ofNat, Subtype.val, _private.0.directSumNeZeroMulEquiv, AddEquiv.symm
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
refine : ∀ (i : { i : ι // n i ≠ 0 }), LT.lt (α := ℕ) 1 ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) i)
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
i : ι
hi : n i ≠ 0
⊢ LT.lt (α := ℕ) 1
    ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i hi))

Tactic:
one_lt_pow₀ (hp _).one_lt hi

Premises used: Nat.Prime.one_lt, one_lt_pow₀
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
ι : Type
hι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
n : ι → ℕ
e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)
i : ι
hi : n i ≠ 0
⊢ LT.lt (α := ℕ) 1
    ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i hi))

Tactic:
exact one_lt_pow₀ (hp _).one_lt hi

Premises used: Nat.Prime.one_lt, one_lt_pow₀
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
obtain :
  ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
    (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)),
    ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
      (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
obtain₁ :
  ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
    (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)) (i : { i : ι // n i ≠ 0 }),
    LT.lt (α := ℕ) 1 ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) i)
obtain₂ :
  ∀ (ι : Type) (hι : Fintype ι) (p : ι → ℕ) (hp : ∀ (i : ι), Nat.Prime (p i)) (n : ι → ℕ)
    (e : G ≃+ ⨁ (i : ι), ZMod (p i ^ n i)) (i : ι) (hi : n i ≠ 0),
    LT.lt (α := ℕ) 1
      ((fun (i : { i : ι // n i ≠ 0 }) ↦ p (↑i : ι) ^ n (↑i : ι)) (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i hi))
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
classical
  obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
  refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
  rintro ⟨i, hi⟩
  exact one_lt_pow₀ (hp _).one_lt hi

Premises used: AddCommGroup.equiv_directSum_zmod_of_finite
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : AddCommGroup G
hG' : AddGroup.FG G
hG : AddMonoid.IsTorsion G
⊢ Finite G

Tactic:
@Module.finite_of_fg_torsion _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG') <|
    AddMonoid.isTorsion_iff_isTorsion_int.mp hG

Premises used: AddMonoid.isTorsion_iff_isTorsion_int, Iff.mp, Module.finite_of_fg_torsion
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u
inst : CommGroup G
inst_1 : Group.FG G
hG : Monoid.IsTorsion G
⊢ Finite G

Tactic:
@Finite.of_equiv _ _ (AddCommGroup.finite_of_fg_torsion (Additive G) hG) Multiplicative.ofAdd

Premises used: Finite.of_equiv, Multiplicative.ofAdd
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Finite G
obtain :
  ∀ (ι : Type) (inst_2 : Fintype ι) (n : ι → ℕ) (h₁ : ∀ (i : ι), 1 < n i)
    (h₂ : Nonempty.{u_1 + 1} (Additive G ≃+ ⨁ (i : ι), ZMod (n i))),
    ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
      (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Tactic:
obtain ⟨ι, inst, n, h₁, h₂⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' (Additive G)

Premises used: AddCommGroup.equiv_directSum_zmod_of_finite', Additive
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst_1 : CommGroup G
inst_2 : Finite G
ι : Type
inst : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (Additive G ≃+ ⨁ (i : ι), ZMod (n i))
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Tactic:
⟨ι, inst, n, h₁, ⟨MulEquiv.toAdditive.symm <| h₂.some.trans <|
    (DirectSum.addEquivProd _).trans (MulEquiv.piMultiplicative _).toAdditiveRight⟩⟩

Premises used: MulEquiv.toAdditiveRight, Nonempty.some, Nonempty.intro, AddEquiv.trans, And.intro, Exists.intro, Equiv.symm, DirectSum.addEquivProd, DFunLike.coe, MulEquiv.toAdditive
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst_1 : CommGroup G
inst_2 : Finite G
ι : Type
inst : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty.{u_1 + 1} (Additive G ≃+ ⨁ (i : ι), ZMod (n i))
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Tactic:
exact ⟨ι, inst, n, h₁, ⟨MulEquiv.toAdditive.symm <| h₂.some.trans <|
    (DirectSum.addEquivProd _).trans (MulEquiv.piMultiplicative _).toAdditiveRight⟩⟩
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst : CommGroup G
hG : Group.FG G
obtain :
  ∀ (n : ℕ) (ι : Type) (inst_1 : Fintype ι) (x : ι → ℕ) (p : ∀ (i : ι), Nat.Prime (x i)) (e : ι → ℕ)
    (equiv : Nonempty.{u_1 + 1} (Additive G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (x i ^ e i))),
    ∃ (ι : Type) (j : Type) (x : Fintype ι) (x : Fintype j) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
      Nonempty.{max 1 (u_1 + 1)} (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))
⊢ ∃ (ι : Type) (j : Type) (x : Fintype ι) (x : Fintype j) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u_1 + 1)} (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))

Tactic:
obtain ⟨n, ι, inst, x, p, e, equiv⟩ := AddCommGroup.equiv_free_prod_directSum_zmod (Additive G)

Premises used: Additive, AddCommGroup.equiv_free_prod_directSum_zmod
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
G : Type u_1
inst_1 : CommGroup G
hG : Group.FG G
n : ℕ
ι : Type
inst : Fintype ι
x : ι → ℕ
p : ∀ (i : ι), Nat.Prime (x i)
e : ι → ℕ
equiv : Nonempty.{u_1 + 1} (Additive G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (x i ^ e i))
⊢ ∃ (ι : Type) (j : Type) (x : Fintype ι) (x : Fintype j) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u_1 + 1)} (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))

Tactic:
exact ⟨ι, Fin n, inst, inferInstance, x, p, e, ⟨MulEquiv.toAdditive.symm <| equiv.some.trans <|
    ((Finsupp.addEquivFunOnFinite.trans <| ((AddEquiv.piAdditive _).trans <|
        (AddEquiv.additiveMultiplicative ℤ).arrowCongr (Equiv.refl _)).symm).prodCongr
          (DirectSum.addEquivProd _ )).trans <| (AddEquiv.prodAdditive _ _).symm⟩⟩
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
A : Type u_1
inst : CommGroup A
inst_1 : Group.FG A
n : ℕ
hn : n ≠ 0
⊢ FiniteIndex.{u_1} (G := A) (MonoidHom.range (G := A) (powMonoidHom n))

Tactic:
finiteIndex_iff_finite_quotient.mpr <| CommGroup.finite_of_fg_torsion _ <|
    CommGroup.isTorsion_quotient_range_powMonoidHom A hn

Premises used: Iff.mpr, Subgroup.finiteIndex_iff_finite_quotient, CommGroup.isTorsion_quotient_range_powMonoidHom, CommGroup.finite_of_fg_torsion
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
rw : (subgroupOf (map (powMonoidHom n) B) B).FiniteIndex
⊢ IsFiniteRelIndex (map (powMonoidHom n) B) B

Tactic:
rw [isFiniteRelIndex_iff_finiteIndex]

Premises used: Subgroup.isFiniteRelIndex_iff_finiteIndex
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
h :
  ∀ (x : ↥B),
    x ∈ subgroupOf (map (powMonoidHom n) B) B ↔ Membership.mem (γ := Subgroup ↥B) (MonoidHom.range (powMonoidHom n)) x
⊢ subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)

Tactic:
ext1
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
x : ↥B
⊢ x ∈ subgroupOf (map (powMonoidHom n) B) B ↔ Membership.mem (γ := Subgroup ↥B) (MonoidHom.range (powMonoidHom n)) x

Tactic:
simp [mem_subgroupOf, Subtype.ext_iff]

Premises used: Subtype.ext_iff, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
A : Type u_1
inst : CommGroup A
B : Subgroup A
hB : B.FG
n : ℕ
hn : n ≠ 0
⊢ subgroupOf (map (powMonoidHom n) B) B = MonoidHom.range (powMonoidHom n)

Tactic:
have : (map (powMonoidHom (α := A) n) B).subgroupOf B = (powMonoidHom (α := B) n).range := by
    ext1
    simp [mem_subgroupOf, Subtype.ext_iff]