diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 176a71f..5a907c8 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -1,3 +1,4 @@
+import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Complex.TaylorSeries
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
@@ -21,17 +22,18 @@ def Harmonic (f : ℂ → ℂ) : Prop :=
 
 #check second_derivative_symmetric
 
-lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℂ, 0 = 1 := by
+lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℝ × ℝ, 0 = 1 := by
   intro z a b
 
-  let fx  := fun w ↦ (fderiv ℝ f w) 1
-  let fxx := fun w ↦ (fderiv ℝ fx w) 1
-  let f2  := (fderiv ℝ (fun w => fderiv ℝ f w) z) 1 1
-
-  have : iteratedFDeriv ℝ (1 + 1) f = 0 := by
-    rw [iteratedFDeriv_succ_eq_comp_left]
+  let fx  := fun w ↦ (fderiv ℝ f w) a
+  let fxx := fun w ↦ (fderiv ℝ fx w) a
+  let f2  := (fderiv ℝ (fun w => fderiv ℝ f w) z) a a
 
+  have :  iteratedFDeriv ℝ 1 f z ![a] = 0 := by
+    rw [iteratedFDeriv_succ_apply_left]
     simp
+    let g := iteratedFDeriv ℝ 0 f
+    simp at g
     sorry
 
   have : f2 = fxx z := by