awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
⊢ Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
              if h : n i = 0 then 0
              else
                DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
              (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
            x)) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))
have of : Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
  ((directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      ((if h : n i = 0 then 0
          else
            DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
              (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        x) :
    ⨁ (i : ι), ZMod (p i ^ n i))
  (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
        (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
      x :
    ⨁ (i : ι), ZMod (p i ^ n i))
Tactic: rw [DirectSum.toAddMonoid_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
⊢ Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          x) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))
have pos : ∀ (h : n i = 0),
  Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((0 : (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) x) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
pos :
  ∀ (h : n i = 0),
    Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
      ((directSumNeZeroMulHom p n :
            (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
          ((0 : (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) x) :
        ⨁ (i : ι), ZMod (p i ^ n i))
      (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
          x :
        ⨁ (i : ι), ZMod (p i ^ n i))
⊢ Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          x) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))
have neg : ∀ (h : ¬n i = 0),
  Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        (((DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
              ZMod
                  (p (↑(Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) : ι) ^
                    n (↑(Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) : ι)) →+
                ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) :
            (a : ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          x) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
⊢ p i ^ n i = 1
have rw : HPow.hPow (β := ℕ) (p i) 0 = 1
Tactic: rw [h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
rw : HPow.hPow (β := ℕ) (p i) 0 = 1
⊢ p i ^ n i = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [h, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
x y : ⨁ (i : ι), ZMod (p i ^ n i)
hx :
  (directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
            if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        x) =
    x
hy :
  (directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
            if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        y) =
    y
⊢ (directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
            if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        (x + y)) =
    x + y
have add : (directSumNeZeroMulHom p n :
      (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
    (HAdd.hAdd (α := ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) (β :=
      ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
              if h : n i = 0 then 0
              else
                DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          x :
        ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
              if h : n i = 0 then 0
              else
                DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          y :
        ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))) =
  x + y
Tactic: rw [map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
x : ⨁ (i : ι), ZMod (p i ^ n i)
⊢ (directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
            if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        x) =
    x
have zero : Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
  ((directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
            if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        0) :
    ⨁ (i : ι), ZMod (p i ^ n i))
  (0 : ⨁ (i : ι), ZMod (p i ^ n i))
Tactic: induction x using DirectSum.induction_on with
    | zero => rw [map_zero, map_zero]
    | of i x =>
      rw [DirectSum.toAddMonoid_of]
      split_ifs with h
      · simp [(ZMod.subsingleton_iff.2 <| by rw [h, pow_zero]).elim x 0]
      · simp_rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of]
    | add x y hx hy => rw [map_add, map_add, hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
x : ⨁ (i : ι), ZMod (p i ^ n i)
zero :
  Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
              if h : n i = 0 then 0
              else
                DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          0) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (0 : ⨁ (i : ι), ZMod (p i ^ n i))
⊢ (directSumNeZeroMulHom p n :
        (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
      ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
            if h : n i = 0 then 0
            else
              DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
          (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
        x) =
    x
have of : ∀ (i : ι) (x : ZMod (p i ^ n i)),
  Eq (α := ⨁ (i : ι), ZMod (p i ^ n i))
    ((directSumNeZeroMulHom p n :
          (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
        ((DirectSum.toAddMonoid (β := fun (i : ι) ↦ ZMod (p i ^ n i)) fun (i : ι) ↦
              if h : n i = 0 then 0
              else
                DirectSum.of (fun (j : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑j : ι) ^ n (↑j : ι)))
                  (Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) i h) :
            (a : ⨁ (i : ι), ZMod (p i ^ n i)) → ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
          (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
              (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
            x)) :
      ⨁ (i : ι), ZMod (p i ^ n i))
    (((DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) i : ZMod (p i ^ n i) →+ ⨁ (i : ι), ZMod (p i ^ n i)) :
          (a : ZMod (p i ^ n i)) → ⨁ (i : ι), ZMod (p i ^ n i))
        x :
      ⨁ (i : ι), ZMod (p i ^ n i))
Tactic: induction x using DirectSum.induction_on with
    | zero => rw [map_zero, map_zero]
    | of i x =>
      rw [DirectSum.toAddMonoid_of]
      split_ifs with h
      · simp [(ZMod.subsingleton_iff.2 <| by rw [h, pow_zero]).elim x 0]
      · simp_rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of]
    | add x y hx hy => rw [map_add, map_add, hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
M : Type u
inst : AddCommGroup M
inst_1 : Module ℤ M
inst_2 : Module.Finite ℤ M
hM : IsTorsion ℤ M
⊢ Finite M
have rcases : ∀ (ι : Type) (w : Fintype ι) (p : ι → ℤ) (h : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ)
  (l : M ≃ₗ[ℤ] ⨁ (i : ι), HasQuotient.Quotient ℤ (B := Submodule ℤ ℤ) (ℤ ∙ p i ^ e i)), Finite M
Tactic: rcases Module.equiv_directSum_of_isTorsion hM with ⟨ι, _, p, h, e, ⟨l⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
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)
⊢ Finite M
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
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
⊢ Finite M
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (hypothesis)
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 M
have this₁ : 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
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u
inst : AddCommGroup G
hG : AddGroup.FG G
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ :=
    @Module.equiv_free_prod_directSum _ _ _ _ _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG)
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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))
have refine_1 : ∀ (i : ι), Nat.Prime ((fun (i : ι) ↦ (p i).natAbs) i)
Tactic: refine ⟨n, ι, fι, fun i => (p i).natAbs, fun i => ?_, e, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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)
⊢ ∃ (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))
have refine_2 : G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (HPow.hPow (α := ℕ) ((fun (i : ι) ↦ (p i).natAbs) i) (e i))
Tactic: refine ⟨n, ι, fι, fun i => (p i).natAbs, fun i => ?_, e, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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 : ι
⊢ Nat.Prime ((fun (i : ι) ↦ (p i).natAbs) i)
have refine_1 : Irreducible (p i)
Tactic: rw [← Int.prime_iff_natAbs_prime, ← irreducible_iff_prime]
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
have 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))
Tactic: cases nonempty_fintype G
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u
inst : AddCommGroup G
inst_1 : Finite G
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))
have 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))
Tactic: obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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)
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
have 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))
Tactic: rcases n with - | n
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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))
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
have 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))
Tactic: rcases n with - | n
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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)
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
have 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))
Tactic: have : Unique (Fin Nat.zero →₀ ℤ) :=
      { uniq := by subsingleton }
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
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)
⊢ ∃ (ι : Type) (x : Fintype ι) (p : ι → ℕ) (_ : ∀ (i : ι), Nat.Prime (p i)) (e : ι → ℕ),
    Nonempty.{max 1 (u + 1)} (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
have 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))
Tactic: haveI := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _
-- Lean 4 proof step from Mathlib.GroupTheory.FiniteAbelian.Basic (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
inst_1 : Finite G
⊢ ∃ (ι : Type) (x : Fintype ι) (n : ι → ℕ),
    (∀ (i : ι), 1 < n i) ∧ Nonempty.{max 1 (u_1 + 1)} (G ≃+ ⨁ (i : ι), ZMod (n i))
have 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))
Tactic: obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G