∀ {R : Type u_3} {n : ℕ} {M : Fin n.succ → Type u_2} {M₂ : Type u_1} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (p : Fin (n + 1)) (f : MultilinearMap R M M₂)
  (x : M p) (m : (i : Fin n) → M (p.succAbove i)) (i : Fin n) (x_1 y : M (p.succAbove i)),
  (fun m => f (p.insertNth x m)) (Function.update m i (x_1 + y)) =
    (fun m => f (p.insertNth x m)) (Function.update m i x_1) + (fun m => f (p.insertNth x m)) (Function.update m i y)