-- 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)
⊢ 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₃ : 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)
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]