-- Module: Mathlib.GroupTheory.FiniteAbelian.Basic
Goal:
ι : Type
inst : DecidableEq ι
p n : ι → ℕ
i : { i : ι // n i ≠ 0 }
x : ZMod (p (↑i : ι) ^ n (↑i : ι))
of :
  Eq (α := ⨁ (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 : ι)))
        ((DirectSum.toAddMonoid (β := fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι)))
              fun (i : { i : ι // n i ≠ 0 }) ↦ DirectSum.of (fun (i : ι) ↦ ZMod (p i ^ n i)) (↑i : ι) :
            (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
          (((DirectSum.of (fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι))) i :
                ZMod (p (↑i : ι) ^ n (↑i : ι)) →+ ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
    (((DirectSum.of (fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι))) i :
            ZMod (p (↑i : ι) ^ n (↑i : ι)) →+ ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
of₁ :
  Eq (α := ⨁ (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 : ι)))
        (((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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
    (((DirectSum.of (fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι))) i :
            ZMod (p (↑i : ι) ^ n (↑i : ι)) →+ ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
of₂ :
  Eq (α := ⨁ (i : { i : ι // n i ≠ 0 }), 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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
    (((DirectSum.of (fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι))) i :
            ZMod (p (↑i : ι) ^ n (↑i : ι)) →+ ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
of₃ of₄ :
  Eq (α := ⨁ (i : { i : ι // n i ≠ 0 }), 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 : ι) ⋯) :
            ZMod
                (p (↑(Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) (↑i : ι) ⋯) : ι) ^
                  n (↑(Subtype.mk (p := fun (i : ι) ↦ n i ≠ 0) (↑i : ι) ⋯) : ι)) →+
              ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
    (((DirectSum.of (fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι))) i :
            ZMod (p (↑i : ι) ^ n (↑i : ι)) →+ ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
⊢ Eq (α := ⨁ (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 : ι)))
        ((directSumNeZeroMulHom p n :
            (a : ⨁ (i : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι))) → ⨁ (i : ι), ZMod (p i ^ n i))
          (((DirectSum.of (fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι))) i :
                ZMod (p (↑i : ι) ^ n (↑i : ι)) →+ ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))
    (((DirectSum.of (fun (i : { i : ι // n i ≠ 0 }) ↦ ZMod (p (↑i : ι) ^ n (↑i : ι))) i :
            ZMod (p (↑i : ι) ^ n (↑i : ι)) →+ ⨁ (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 : { i : ι // n i ≠ 0 }), ZMod (p (↑i : ι) ^ n (↑i : ι)))

Tactic:
rw [directSumNeZeroMulHom, DirectSum.toAddMonoid_of, DirectSum.toAddMonoid_of,
        dif_neg i.prop]

Premises used: dif_neg, Subtype.prop, _private.0.directSumNeZeroMulHom, DirectSum.toAddMonoid_of