-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem norm_eval_le_injectiveSeminorm (f : ContinuousMultilinearMap 𝕜 E F) (x : ⨂[𝕜] i, E i) :
    ‖lift f.toMultilinearMap x‖ ≤ ‖f‖ * injectiveSeminorm x

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)
G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)
e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜]
  ↥(LinearMap.range (lift f.toMultilinearMap)) :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
hle :
  (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ injectiveSeminorm
⊢ ‖(lift f'.toMultilinearMap) x‖ ≤ ‖f'‖ * injectiveSeminorm x

Tactic:
refine le_trans ?_ (mul_le_mul_of_nonneg_left (hle x) (norm_nonneg f'))

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)
G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)
e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜]
  ↥(LinearMap.range (lift f.toMultilinearMap)) :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
hle :
  (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ injectiveSeminorm
⊢ ‖(lift f'.toMultilinearMap) x‖ ≤
    ‖f'‖ *
      (fun f => ⇑f) ((normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G))
        x

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)
G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)
e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜]
  ↥(LinearMap.range (lift f.toMultilinearMap)) :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
⊢ (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ∈
    {p |
      ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}

Tactic:
rw [Set.mem_setOf]

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
G : Type (max (max (max uE u𝕜) uι) (max uE uι) u𝕜) := (⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)
G' : Submodule 𝕜 F := LinearMap.range (lift f.toMultilinearMap)
e : ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) ≃ₗ[𝕜]
  ↥(LinearMap.range (lift f.toMultilinearMap)) :=
  (lift f.toMultilinearMap).quotKerEquivRange
this✝ : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G (↥G') e
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G (↥G') e
f'₀ : MultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  lift.symm (↑e.symm ∘ₗ (lift f.toMultilinearMap).rangeRestrict)
hf'₀ : ∀ (x : (i : ι) → E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖
f' : ContinuousMultilinearMap 𝕜 E ((⨂[𝕜] (i : ι), E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)) :=
  f'₀.mkContinuous ‖f‖ hf'₀
hnorm : ‖f'‖ ≤ ‖f‖
heq : ↑(e ((lift f'.toMultilinearMap) x)) = (lift f.toMultilinearMap) x
⊢ ∃ G_1 x x_1,
    (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) =
      (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G_1 →L[𝕜] G_1)).comp (toDualContinuousMultilinearMap G_1)