-- 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
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
add₁ :
  HAdd.hAdd (α := ⨁ (i : ι), ZMod (p i ^ n i)) (β := ⨁ (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) :
        ⨁ (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 : ι)))
            y) :
        ⨁ (i : ι), ZMod (p i ^ n i)) =
    x + y
add₂ :
  HAdd.hAdd (β := ⨁ (i : ι), ZMod (p i ^ n i)) x
      ((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) :
        ⨁ (i : ι), ZMod (p i ^ n i)) =
    x + 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₃ : x + y = x + y
Tactic: rw [map_add, map_add, hx, hy]