-- Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
Goal:
ι : Type uι
inst : Fintype ι
𝕜 : Type u𝕜
E : ι → Type uE
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedSpace.{u𝕜, uE} 𝕜 (E i)
G : Type u_1
inst_4 : SeminormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x_1 : (↑(x.lifts (s := E)) : Type (max (max uE uι) u𝕜))
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts (s := E)
grw :
  Multiset.sum
      (Multiset.map (fun (x : G) ↦ ‖x‖)
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
              Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
                (lifts (s := E)
                  (List.sum
                    (List.map
                      (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                        p))))
                x)
              p ⋯) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖
⊢ norm.{u_1} (E := G)
      (Multiset.sum
        (↑(List.map (α := 𝕜 × ((i : ι) → E i))
              (Function.comp (β := ⨂[𝕜] (i : ι), E i)
                (⇑((lift (s := E) : (a : MultilinearMap 𝕜 E G) → (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G)
                        (f.toMultilinearMap (M₁ := E)) :
                      (⨂[𝕜] (i : ι), E i) →ₗ[𝕜] G) :
                  (a : ⨂[𝕜] (i : ι), E i) → G)
                fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
              ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i))) p)) :
          Multiset G)) ≤
    projectiveSeminormAux (E := E)
        (↑(Subtype.mk (p := fun (x : FreeAddMonoid (𝕜 × ((i : ι) → E i))) ↦
              Membership.mem (γ := Set (FreeAddMonoid (𝕜 × ((i : ι) → E i))))
                (lifts (s := E)
                  (List.sum
                    (List.map
                      (fun (x : 𝕜 × ((i : ι) → E i)) ↦ HSMul.hSMul (β := ⨂[𝕜] (i : ι), E i) x.1 (⨂ₜ[𝕜] (i : ι), x.2 i))
                      ((FreeAddMonoid.toList : (a : FreeAddMonoid (𝕜 × ((i : ι) → E i))) → List (𝕜 × ((i : ι) → E i)))
                        p))))
                x)
              p ⋯) :
          FreeAddMonoid (𝕜 × ((i : ι) → E i))) *
      ‖f‖

Tactic:
grw [norm_multiset_sum_le]

Premises used: norm_multiset_sum_le