-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Semiring S
inst_7 : Module S N
inst_8 : SMulCommClass R S N
F : (i : ι) → LinearMap.{u_3, u_3, u_5, u_6} (RingHom.id R) (M i) N
c : R
f_1 : Π₀ (i : ι), M i
a : ι
b : M a
f : Π₀ (i : ι), M i
h : (f : (a : ι) → M a) a = 0
h_1 : b ≠ 0
hf :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) =
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
ha :
  (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
      (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b) + c • f) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) :
        N)
ha₁ :
  HAdd.hAdd (α := N) (β := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
        N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) :
        N)
ha₂ :
  HAdd.hAdd (α := N) (β := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
        N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
    c •
      HAdd.hAdd (α := N) (β := N)
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) : N)
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
ha₃ :
  HAdd.hAdd (α := N) (β := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
        N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • f) : N) =
    HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) :
          N) +
      HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
ha₄ :
  HAdd.hAdd (α := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N)
          (HSMul.hSMul (β := Π₀ (i : ι), M i) c (single (β := M) a b)) :
        N)
      (HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)) =
    HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) :
          N) +
      HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
ha₅ :
  HAdd.hAdd (α := N)
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a (c • b)) :
        N)
      (HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)) =
    HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) :
          N) +
      HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
ha₆ :
  HAdd.hAdd (α := N) (((F a).toAddMonoidHom : (a : M a) → N) (c • b) : N)
      (HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)) =
    HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b) :
          N) +
      HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
ha₇ :
  HAdd.hAdd (α := N) (((F a).toAddMonoidHom : (a : M a) → N) (c • b) : N)
      (HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)) =
    HSMul.hSMul (β := N) c (((F a).toAddMonoidHom : (a : M a) → N) b : N) +
      HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
ha₈ :
  HAdd.hAdd (α := N) ((F a : (a : M a) → N) (c • b) : N)
      (HSMul.hSMul (β := N) c
        ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)) =
    HSMul.hSMul (β := N) c ((F a : (a : M a) → N) b : N) +
      HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
⊢ (sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (c • (single (β := M) a b + f)) =
    HSMul.hSMul (β := N) c
      ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) (single (β := M) a b + f) :
        N)
have ha₉ : HSMul.hSMul (β := N) c ((F a : (a : M a) → N) b : N) +
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N) =
  HSMul.hSMul (β := N) c ((F a : (a : M a) → N) b : N) +
    HSMul.hSMul (β := N) c ((sumAddHom (β := M) fun (i : ι) ↦ (F i).toAddMonoidHom : (a : Π₀ (i : ι), M i) → N) f : N)
Tactic: rw [smul_add, map_add, map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            map_smul]