-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 ι
x y : 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)
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (x + y) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (x + y) (some i)).2 i) =
    HAdd.hAdd (α := F) (β := F)
      ((((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) y none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) y (some i)).2 i :
        F)
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) (x + y) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (x + y) (some i)).2 i) =
    HAdd.hAdd (α := F) (β := F)
      ((((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) y none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) y (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]