-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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
⊢ 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‖) ⋯)
have 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' := sorry, map_smul' := sorry }
            (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) sorry :
          (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' := sorry, map_smul' := sorry : G →ₗ[𝕜] G' }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) sorry)
            (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' := sorry, map_smul' := sorry : G →ₗ[𝕜] G' }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i y i_1‖) sorry) :
          (a : G) → G')
        x_1 :
      G')
Tactic: ext1