-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
have :
  ∀ (z : G × ((i : ι) → E i)),
    (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
      update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)
have₁ :
  ∀
    (B_1 :
      ∀ (z : G × ((i : ι) → E i)),
        (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
          update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)),
    ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
              (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
            ContinuousMultilinearMap 𝕜 E F) :
          (a : (i : ι) → E i) → F)
        fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
      HSMul.hSMul (β := F) c
        ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                  (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x none).1 :
                ContinuousMultilinearMap 𝕜 E F) :
              (a : (i : ι) → E i) → F)
            fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
          F)
have₂ :
  ∀ (z : G × ((i : ι) → E i)),
    (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
      update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)
have₃ have₄ :
  ∀
    (B_1 :
      ∀ (z : G × ((i : ι) → E i)),
        (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
          update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)),
    ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
              (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
            ContinuousMultilinearMap 𝕜 E F) :
          (a : (i : ι) → E i) → F)
        fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
      HSMul.hSMul (β := F) c
        ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                  (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x none).1 :
                ContinuousMultilinearMap 𝕜 E F) :
              (a : (i : ι) → E i) → F)
            fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
          F)
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
        F)

Tactic:
classical
        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
        simp [B]