-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
h :
  ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
              (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          (erase (β := fun (i : ι) ↦ ↥(p i)) i v) =
        (↑x : N) →
      x = 0
m : Π₀ (i : ι), ↥(p i)
hm :
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        m :
      N)
    (0 : N)
i : ι
h₁ :
  ∀
    (hm :
      Eq.{u_6 + 1} (α := N)
        (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype :
              (a : Π₀ (i : ι), ↥(p i)) → N)
            (erase (β := fun (i : ι) ↦ ↥(p i)) i m + single (β := fun (i : ι) ↦ ↥(p i)) i ((m : (a : ι) → ↥(p a)) i)) :
          N)
        (0 : N)),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (erase (β := fun (i : ι) ↦ ↥(p i)) i m) =
      (↑(-(m : (a : ι) → ↥(p a)) i) : N)
h₂ :
  ∀
    (hm :
      HAdd.hAdd (α := N) (β := N)
          (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                  fun (i : ι) ↦ (p i).subtype :
                (a : Π₀ (i : ι), ↥(p i)) → N)
              (erase (β := fun (i : ι) ↦ ↥(p i)) i m) :
            N)
          (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                  fun (i : ι) ↦ (p i).subtype :
                (a : Π₀ (i : ι), ↥(p i)) → N)
              (single (β := fun (i : ι) ↦ ↥(p i)) i ((m : (a : ι) → ↥(p a)) i)) :
            N) =
        0),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (erase (β := fun (i : ι) ↦ ↥(p i)) i m) =
      (↑(-(m : (a : ι) → ↥(p a)) i) : N)
h₃ :
  ∀
    (hm :
      HAdd.hAdd (α := N) (β := N)
          (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                  fun (i : ι) ↦ (p i).subtype :
                (a : Π₀ (i : ι), ↥(p i)) → N)
              (erase (β := fun (i : ι) ↦ ↥(p i)) i m) :
            N)
          (((p i).subtype : (a : ↥(p i)) → N) ((m : (a : ι) → ↥(p a)) i) : N) =
        0),
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        (erase (β := fun (i : ι) ↦ ↥(p i)) i m) =
      (↑(-(m : (a : ι) → ↥(p a)) i) : N)
⊢ ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
          (p i).subtype :
        (a : Π₀ (i : ι), ↥(p i)) → N)
      (erase (β := fun (i : ι) ↦ ↥(p i)) i m) =
    (↑(-(m : (a : ι) → ↥(p a)) i) : N)
have h₄ : ∀
  (hm :
    HAdd.hAdd (α := N)
        (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype :
              (a : Π₀ (i : ι), ↥(p i)) → N)
            (erase (β := fun (i : ι) ↦ ↥(p i)) i m) :
          N)
        (↑((m : (a : ι) → ↥(p a)) i) : N) =
      0),
  ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
          (p i).subtype :
        (a : Π₀ (i : ι), ↥(p i)) → N)
      (erase (β := fun (i : ι) ↦ ↥(p i)) i m) =
    (↑(-(m : (a : ι) → ↥(p a)) i) : N)
Tactic: rwa [← erase_add_single i m, map_add, lsum_single, Submodule.subtype_apply,
    add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm
Cleared hypotheses: hm