feat: two lemmas about ContinuousMultilinearMap (#36188)

* Rename `continuousMultilinearCurryFin0_symm_apply` and remove its simp-lemma (simp can now prove it using the new simp-lemma)
* Add a new version of `continuousMultilinearCurryFin0_symm_apply`.
* The new lemma is very similar to the old one, and these lemmas are most likely to be used only by `simp`, so I don't think a deprecation cycle is needed.
* Also add `ContinuousMultilinearMap.fin0_apply_enorm`

Used for Sobolev spaces.

Author: fpvandoorn

Mathlib/Analysis/Normed/Module/Multilinear/Curry.lean

@@ -455,6 +455,11 @@ theorem ContinuousMultilinearMap.fin0_apply_norm (f : G [×0]→L[𝕜] G') {x :
       simp [-ContinuousMultilinearMap.apply_zero_uncurry0]
   simpa [-Matrix.zero_empty] using this
 
+@[simp]
+theorem ContinuousMultilinearMap.fin0_apply_enorm (f : G [×0]→L[𝕜] G') {x : Fin 0 → G} :
+    ‖f x‖ₑ = ‖f‖ₑ := by
+  simp_rw [← ofReal_norm, fin0_apply_norm]
+
 theorem ContinuousMultilinearMap.curry0_norm (f : G [×0]→L[𝕜] G') : ‖f.curry0‖ = ‖f‖ := by simp
 
 variable (𝕜 G G')
@@ -481,7 +486,11 @@ theorem continuousMultilinearCurryFin0_apply (f : G [×0]→L[𝕜] G') :
   rfl
 
 @[simp]
-theorem continuousMultilinearCurryFin0_symm_apply (x : G') (v : Fin 0 → G) :
+theorem continuousMultilinearCurryFin0_symm_apply (x : G') :
+    (continuousMultilinearCurryFin0 𝕜 G G').symm x = ContinuousMultilinearMap.uncurry0 𝕜 G x :=
+  rfl
+
+theorem continuousMultilinearCurryFin0_symm_apply_apply (x : G') (v : Fin 0 → G) :
     (continuousMultilinearCurryFin0 𝕜 G G').symm x v = x :=
   rfl