-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Basic (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
a b : M₁ (↑i : ι)
repeat repeat₁ repeat₂ :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i (a + b) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
have repeat₃ : (f : (a : (i : ι) → M₁ i) → M₂)
    (update (β := M₁)
      (fun (j : ι) ↦
        if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
      (↑i : ι) (a + b)) =
  HAdd.hAdd (α := M₂) (β := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂)
        (update (β := M₁)
          (fun (j : ι) ↦
            if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
            else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
          (↑i : ι) a) :
      M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if h : P j then
          update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
        else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
      M₂)
Tactic: classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_add]