-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
inst_11 : DecidableEq ι
m : (i : ι) → E i
i : ι
x y : E i
h :
  ∀ (x_1 : G),
    Eq.{wG' + 1} (α := G')
      ((LinearMap.mkContinuous
              {
                toFun := fun (x_2 : G) ↦
                  (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                      (a : (i : ι) → E i) → G')
                    (update (β := E) m i (x + y)),
                map_add' := ⋯, map_smul' := ⋯ }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) ⋯ :
            (a : G) → G')
          x_1 :
        G')
      ((HAdd.hAdd (α := G →L[𝕜] G')
              (LinearMap.mkContinuous
                {
                  toFun := fun (x_2 : G) ↦
                    (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                        (a : (i : ι) → E i) → G')
                      (update (β := E) m i x),
                  map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
                (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯)
              (LinearMap.mkContinuous
                {
                  toFun := fun (x : G) ↦
                    (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                        (a : (i : ι) → E i) → G')
                      (update (β := E) m i y),
                  map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
                (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i y i_1‖) ⋯) :
            (a : G) → G')
          x_1 :
        G')
⊢ LinearMap.mkContinuous
      {
        toFun := fun (x_1 : G) ↦
          (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_1 : ContinuousMultilinearMap 𝕜 E G') :
              (a : (i : ι) → E i) → G')
            (update (β := E) m i (x + y)),
        map_add' := ⋯, map_smul' := ⋯ }
      (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) ⋯ =
    HAdd.hAdd (α := G →L[𝕜] G')
      (LinearMap.mkContinuous
        {
          toFun := fun (x_1 : G) ↦
            (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_1 : ContinuousMultilinearMap 𝕜 E G') :
                (a : (i : ι) → E i) → G')
              (update (β := E) m i x),
          map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
        (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯)
      (LinearMap.mkContinuous
        {
          toFun := fun (x : G) ↦
            (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                (a : (i : ι) → E i) → G')
              (update (β := E) m i y),
          map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
        (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i y i_1‖) ⋯)

Tactic:
ext1