-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : ι) → AddCommGroup (M₁ i)
inst_2 : AddCommGroup M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
x h h' : (i : ι) → M₁ i
simp_rw :
  HSub.hSub (β := M₂)
      (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
            ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂) +
          ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) -
        (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
            ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂) +
          ∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x)))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
simp_rw₁ :
  HSub.hSub (β := M₂)
      (HAdd.hAdd (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
          (HAdd.hAdd (α := M₂) (β := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂)
            (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)) -
        HAdd.hAdd (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
          (HAdd.hAdd (α := M₂) (β := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂)
            (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
simp_rw₂ :
  HSub.hSub (β := M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) +
        (HSub.hSub (α := M₂) (β := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂)
            ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂) +
          HSub.hSub (α := M₂) (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x))
            (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x))))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
simp_rw₃ :
  HSub.hSub (β := M₂)
      (0 +
        (HSub.hSub (α := M₂) (β := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂)
            ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂) +
          HSub.hSub (α := M₂) (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x))
            (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x))))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
simp_rw₄ :
  HSub.hSub (β := M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h : M₂)
          ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) h' : M₂) +
        HSub.hSub (α := M₂) (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x))
          (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x)))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
⊢ HSub.hSub (β := M₂)
      (HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (x + h) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (x + h') : M₂))
      ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
    ∑ s : Finset ι with 2 ≤ #s,
      HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
have simp_rw₅ : HSub.hSub (β := M₂)
    (HAdd.hAdd (α := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂)
      (HSub.hSub (α := M₂) (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x))
        (∑ s : Finset ι with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x))))
    ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) (h - h') : M₂) =
  ∑ s : Finset ι with 2 ≤ #s,
    HSub.hSub (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h' x) : M₂)
Tactic: simp_rw [map_add_eq_map_add_linearDeriv_add, add_assoc, add_sub_add_comm, sub_self, zero_add,
    ← map_sub, add_sub_cancel_left, sum_sub_distrib]