-- Mathlib/GroupTheory/FiniteAbelian/Basic.lean
theorem equiv_directSum_zmod_of_finite [Finite G] :
    ∃ (ι : Type) (_ : Fintype ι) (p : ι → ℕ) (_ : ∀ i, Nat.Prime <| p i) (e : ι → ℕ),
      Nonempty <| G ≃+ ⨁ i : ι, ZMod (p i ^ e i)

Proof state:
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 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Unique (Fin Nat.zero →₀ ℤ)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

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

Result:
no goals

Proof state:
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, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
rcases n with - | n

Result:
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 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

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 (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Proof state:
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 (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Fintype (Fin (n + 1) →₀ ℤ)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (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

Result:
no goals

Proof state:
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 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∀ (a : Fin Nat.zero →₀ ℤ), a = default

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
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 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ (Fin Nat.zero →₀ ℤ) → True

Proof state:
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
cases nonempty_fintype G

Result:
case intro
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Proof state:
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 (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
haveI := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _

Result:
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 (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Fintype (Fin (n + 1) →₀ ℤ)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Proof state:
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 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
have : Unique (Fin Nat.zero →₀ ℤ) :=
  { uniq := by simp only [eq_iff_true_of_subsingleton]; trivial }

Result:
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 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Unique (Fin Nat.zero →₀ ℤ)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Proof state:
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 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ (Fin Nat.zero →₀ ℤ) → True

Tactic:
trivial

Result:
no goals

Proof state:
case intro
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

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

Result:
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, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))