-- Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
theorem norm_eval_le_projectiveSeminorm (x : ⨂[𝕜] i, E i) (G : Type*) [SeminormedAddCommGroup G]
    [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖lift f.toMultilinearMap x‖ ≤ projectiveSeminorm x * ‖f‖

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
this : Nonempty (Subtype (Membership.mem x.lifts)) := nonempty_subtype.mpr (nonempty_lifts x)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp✝ : p ∈ x.lifts
hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x
⊢ (Multiset.map (fun x => ‖x‖) ↑(List.map (⇑(lift f.toMultilinearMap) ∘ fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p)).sum ≤
    (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑⟨p, hp✝⟩ * ‖f‖

Tactic:
simp only [tprodCoeff_eq_smul_tprod, Multiset.map_coe, List.map_map, Multiset.sum_coe,
  Function.comp_apply]

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
this : Nonempty (Subtype (Membership.mem x.lifts)) := nonempty_subtype.mpr (nonempty_lifts x)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp✝ : p ∈ x.lifts
hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x
⊢ (List.map ((fun x => ‖x‖) ∘ ⇑(lift f.toMultilinearMap) ∘ fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum ≤
    (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum * ‖f‖

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
this : Nonempty (Subtype (Membership.mem x.lifts)) := nonempty_subtype.mpr (nonempty_lifts x)
⊢ ∀ (x_1 : ↑x.lifts), ‖(lift f.toMultilinearMap) x‖ ≤ (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑x_1 * ‖f‖

Tactic:
intro ⟨p, hp⟩

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
this : Nonempty (Subtype (Membership.mem x.lifts)) := nonempty_subtype.mpr (nonempty_lifts x)
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑⟨p, hp⟩ * ‖f‖

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
this : Nonempty (Subtype (Membership.mem x.lifts)) := nonempty_subtype.mpr (nonempty_lifts x)
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ projectiveSeminorm x * ‖f‖

Tactic:
rw [projectiveSeminorm_apply, Real.iInf_mul_of_nonneg (norm_nonneg _), projectiveSeminormAux]

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
x : ⨂[𝕜] (i : ι), E i
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
this : Nonempty (Subtype (Membership.mem x.lifts)) := nonempty_subtype.mpr (nonempty_lifts x)
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ⨅ i, (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑i * ‖f‖