-- 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 : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : Equiv.{u_1 + 1, uι + 1} α (↑s : Type uι)
inst_9 : DecidablePred fun (x : ι) ↦ x ∈ s
inst_10 : DecidableEq { a : ι // a ∉ s }
m : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)
i : { a : ι // a ∉ s }
x y : M₁ (↑i : ι)
⊢ mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
      (fun (v : (i : α) → (i : ι) → M₁ i) ↦
        (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                  (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                    MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i (x + y)) :
              MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
            (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
          fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
      ⋯ ⋯ =
    HAdd.hAdd (α := MultilinearMap R (fun (x : α) ↦ (i : ι) → M₁ i) M₂)
      (mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
        (fun (v : (i : α) → (i : ι) → M₁ i) ↦
          (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i x) :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
        ⋯ ⋯)
      (mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
        (fun (v : (i : α) → (i : ι) → M₁ i) ↦
          (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i y) :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
        ⋯ ⋯)
have H : ∀ (x_1 : (i : α) → (i : ι) → M₁ i),
  Eq.{v₂ + 1} (α := M₂)
    ((mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
            (fun (v : (i : α) → (i : ι) → M₁ i) ↦
              (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                        (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                          MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                      (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i (x + y)) :
                    MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
                  (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
                fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
            sorry sorry :
          (a : (i : α) → (i : ι) → M₁ i) → M₂)
        x_1 :
      M₂)
    ((HAdd.hAdd (α := MultilinearMap R (fun (x : α) ↦ (i : ι) → M₁ i) M₂)
            (mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
              (fun (v : (i : α) → (i : ι) → M₁ i) ↦
                (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                          (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                            MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                        (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i x) :
                      MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
                    (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
                  fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
              sorry sorry)
            (mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
              (fun (v : (i : α) → (i : ι) → M₁ i) ↦
                (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                          (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                            MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                        (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i y) :
                      MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
                    (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
                  fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
              sorry sorry) :
          (a : (i : α) → (i : ι) → M₁ i) → M₂)
        x_1 :
      M₂)
Tactic: ext