From ecdc182f2b76661be8b3aad96bf9f8769b0a712b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 24 Jun 2024 08:03:39 +0200
Subject: [PATCH] Update laplace2.lean

---
 Nevanlinna/laplace2.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
index f36cb58..c87fa76 100644
--- a/Nevanlinna/laplace2.lean
+++ b/Nevanlinna/laplace2.lean
@@ -61,10 +61,12 @@ theorem LaplaceIndep
   have g : (i : Fin 2) → ι → E := by exact fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j))
   have A : (i : Fin 2) → Finset ι := by exact fun _ ↦ Finset.univ
 
-  let X := ContinuousMultilinearMap.map_sum_finset 
+  let X := ContinuousMultilinearMap.map_sum
     (iteratedFDeriv ℝ 2 f z)
     (fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j)))
-    (fun _ ↦ Finset.univ)
+
+  --
+  --  (fun _ ↦ Finset.univ)
   simp at X
   
   sorry