-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
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
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)) ⋯ :
              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) ⋯ :
                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) :
            (a : ContinuousMultilinearMap 𝕜 E F) → F)
          x_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)) ⋯ =
    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)

Tactic:
ext