-- 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)
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x

Tactic:
set e := LinearMap.quotKerEquivRange (lift f.toMultilinearMap)

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
⊢ ‖(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‖
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * injectiveSeminorm x

Tactic:
set f' := MultilinearMap.mkContinuous f'₀ ‖f‖ hf'₀

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'₀
⊢ ‖(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
⊢ (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤ injectiveSeminorm

Tactic:
simp only [injectiveSeminorm]

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
⊢ (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) ≤
    sSup
      {p |
        ∃ G x x_1,
          p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}