-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.Defs (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
N : Type u_3
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
ι : Type u_4
R : Type u_5
M : Type u_6
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
f : End (End R M) M
g : End R (ι →₀ M)
x x_1 x_2 : ι →₀ M
h :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_1 : ι →₀ M)
h' :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_2 : ι →₀ M)
rw :
  (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1 + g • x_2) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
rw₁ :
  HAdd.hAdd (α := ι →₀ M) (β := ι →₀ M)
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_1) : ι →₀ M)
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) : ι →₀ M) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
rw₂ :
  HAdd.hAdd (β := ι →₀ M)
      (HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
        ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
        ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_1 : ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • x_2) : ι →₀ M) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
⊢ (mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (g • (x_1 + x_2)) =
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
have rw₃ : HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_1 : ι →₀ M) +
    HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
      ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
      ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) x_2 : ι →₀ M) =
  HSMul.hSMul (α := End R (ι →₀ M)) (β := ι →₀ M)
    ((RingHom.id (End R (ι →₀ M)) : (a : End R (ι →₀ M)) → End R (ι →₀ M)) g : End R (ι →₀ M))
    ((mapRange.addMonoidHom (↑f : M →+ M) : (a : ι →₀ M) → ι →₀ M) (x_1 + x_2) : ι →₀ M)
Tactic: rw [smul_add, map_add, h, h', map_add, smul_add]