-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm (goal)
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type uE
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
F : Type uF
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
x y : ⨂[𝕜] (i : ι), E i
⊢ LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
      ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
            (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
          (x + y) ∘ₗ
        ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
      ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (x + y)) ⋯ =
    HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
      (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
          ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
              x ∘ₗ
            ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
          ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) ⋯ :
        ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
      (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
          ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
              y ∘ₗ
            ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
          ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) y) ⋯ :
        ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
have h : ∀ (x_1 : ContinuousMultilinearMap 𝕜 E F),
  Eq.{uF + 1} (α := F)
    (((LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
              ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                    (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                  (x + y) ∘ₗ
                ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
              ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) (x + y)) sorry :
            ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)
    ((HAdd.hAdd (α := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) (β := ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
            (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                      (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                    x ∘ₗ
                  ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) x) sorry :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] F)
            (LinearMap.mkContinuous (𝕜 := 𝕜) (𝕜₂ := 𝕜) (F := F) (σ := RingHom.id 𝕜)
                ((LinearMap.flip (↑(lift (s := E)) : MultilinearMap 𝕜 E F →ₗ[𝕜] (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] F) :
                      (a : ⨂[𝕜] (i : ι), E i) → MultilinearMap 𝕜 E F →ₗ[𝕜] F)
                    y ∘ₗ
                  ContinuousMultilinearMap.toMultilinearMapLinear (M₁ := E))
                ((projectiveSeminorm (E := E) : (a : ⨂[𝕜] (i : ι), E i) → ℝ) y) sorry :
              ContinuousMultilinearMap 𝕜 E F →L[𝕜] F) :
          (a : ContinuousMultilinearMap 𝕜 E F) → F)
        x_1 :
      F)
Tactic: ext