From c6b2989c2d0c6c95ec568a43b3b6d85db0ba68cb Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Fri, 20 Dec 2024 13:00:26 +0100
Subject: [PATCH] Try to prove norm_map'

---
 DeRhamCohomology/Alternating/Basic.lean              | 4 ++--
 DeRhamCohomology/ContinuousAlternatingMap/Curry.lean | 2 +-
 DeRhamCohomology/Multilinear/Basic.lean              | 5 ++++-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/DeRhamCohomology/Alternating/Basic.lean b/DeRhamCohomology/Alternating/Basic.lean
index 6714423..690209d 100644
--- a/DeRhamCohomology/Alternating/Basic.lean
+++ b/DeRhamCohomology/Alternating/Basic.lean
@@ -19,8 +19,8 @@ variable
 
 def _root_.LinearIsometryEquiv.flipAlternating :
     (M' →L[𝕜] (M [⋀^ι]→L[𝕜] N)) ≃ₗᵢ[𝕜] (M [⋀^ι]→L[𝕜] (M' →L[𝕜] N)) where
-  toFun f := ContinuousLinearMap.flipAlternating f
-  invFun := sorry
+  toFun := ContinuousLinearMap.flipAlternating
+  invFun f := sorry
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
   left_inv := sorry
diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean b/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
index d030e64..8a609ef 100644
--- a/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
+++ b/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
@@ -83,7 +83,7 @@ theorem uncurryFin_uncurryFinCLM_comp_of_symmetric {f : E →L[𝕜] E →L[𝕜
     Fin.succAbove_succAbove_predAbove, Fin.neg_one_pow_succAbove_add_predAbove, pow_succ',
     neg_one_mul, neg_smul, Fin.removeNth_apply, add_neg_cancel]
 
-def uncurrySum (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) : E [⋀^ι ⊕ ι']→L[𝕜] F := by sorry
+def uncurrySum (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) : E [⋀^ι ⊕ ι']→L[𝕜] F := sorry
 
 def uncurryFinAdd (f : E [⋀^Fin m]→L[𝕜] E [⋀^Fin n]→L[𝕜] F) : E [⋀^Fin (m + n)]→L[𝕜] F := by sorry
 
diff --git a/DeRhamCohomology/Multilinear/Basic.lean b/DeRhamCohomology/Multilinear/Basic.lean
index 955f4e5..bee44bf 100644
--- a/DeRhamCohomology/Multilinear/Basic.lean
+++ b/DeRhamCohomology/Multilinear/Basic.lean
@@ -68,4 +68,7 @@ def LinearIsometryEquiv.flipMultilinear :
   map_smul' _ _ := rfl
   left_inv := congrFun rfl
   right_inv := congrFun rfl
-  norm_map' := fun x => by sorry -- TODO
+  norm_map' := fun f => by
+    simp
+    simp_rw[ContinuousLinearMap.flipMultilinear, MultilinearMap.mkContinuous, LinearMap.mkContinuous]
+    sorry