-- 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 : (i : ι) → M₁ i
simp_rw :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 < 2,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₁ :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 ≤ 1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₂ :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 < 1 ∨ #x_1 = 1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₃ :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with #x_1 = 0 ∨ #x_1 = 1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₄ :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ {a ∈ Finset.powerset Finset.univ | #a = 0} ∪ {a ∈ Finset.powerset Finset.univ | #a = 1},
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₅ :
  HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ powersetCard 0 Finset.univ ∪ powersetCard 1 Finset.univ,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₆ :
  ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
      HAdd.hAdd (α := M₂)
        (∑ x_1 ∈ powersetCard 0 Finset.univ, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
        (∑ x_1 ∈ powersetCard 1 Finset.univ, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₇ :
  ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
      HAdd.hAdd (α := M₂) (∑ x_1 ∈ {∅}, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
        (∑ x_1 ∈ powersetCard 1 Finset.univ, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₈ :
  ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
      HAdd.hAdd (α := M₂) (∑ x_1 ∈ {∅}, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
        (∑ x_1 ∈ map { toFun := singleton, inj' := ⋯ : ι ↪ Finset ι } Finset.univ,
          (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₉ :
  ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
      HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (Finset.piecewise (π := M₁) ∅ h x) : M₂)
        (∑ x_1 ∈ map { toFun := singleton, inj' := ⋯ : ι ↪ Finset ι } Finset.univ,
            (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) :
          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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₁₀ :
  ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
      HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        (∑ x_1 ∈ map { toFun := singleton, inj' := ⋯ : ι ↪ Finset ι } Finset.univ,
            (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) :
          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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₁₁ :
  ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
      HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        (∑ x_1 : ι,
            (f : (a : (i : ι) → M₁ i) → M₂)
              (Finset.piecewise (π := M₁) (({ toFun := singleton, inj' := ⋯ : ι ↪ Finset ι } : (a : ι) → Finset ι) x_1)
                h x) :
          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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
simp_rw₁₂ :
  ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
      HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
        (∑ x_1 : ι, (f : (a : (i : ι) → M₁ i) → M₂) (Finset.piecewise (π := M₁) {x_1} h x) : 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₂) +
      ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
⊢ HAdd.hAdd (α := M₂)
      (∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x))
      (∑ x_1 ∈ Finset.powerset Finset.univ with ¬2 ≤ #x_1,
        (f : (a : (i : ι) → M₁ i) → M₂) (x_1.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.powerset Finset.univ with 2 ≤ #s, (f : (a : (i : ι) → M₁ i) → M₂) (s.piecewise (π := M₁) h x)
have simp_rw₁₃ : ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x) +
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
      (∑ x_1 : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x x_1 (h x_1)) : 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₂) +
    ∑ x_1 ∈ Finset.powerset Finset.univ with 2 ≤ #x_1, (f : (a : (i : ι) → M₁ i) → M₂) (x_1.piecewise (π := M₁) h x)
Tactic: simp_rw [not_le, Nat.lt_succ_iff, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or,
    ← powersetCard_eq_filter, sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one),
    powersetCard_zero, powersetCard_one, sum_singleton, Finset.piecewise_empty, sum_map,
    Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply, add_comm]