diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 828a180..05d0ae1 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -17,18 +17,6 @@ noncomputable def Complex.laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
 def Harmonic (f : ℂ → ℝ) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
-#check contDiff_iff_ftaylorSeries.2
-
-lemma c2_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℂ 2 f := by
-  intro fHyp
-  exact Differentiable.contDiff fHyp
-
-lemma c2R_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℝ 2 f := by
-  intro fHyp
-  let ZZ := c2_if_holomorphic f fHyp
-  apply ContDiff.restrict_scalars ℝ ZZ
-
-
 
 theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
   Differentiable ℂ f → Harmonic (Complex.reCLM ∘ f) := by
@@ -41,7 +29,7 @@ theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
     · -- Complex.reCLM is two times real continuously differentiable
       exact ContinuousLinearMap.contDiff Complex.reCLM
     · -- f is two times real continuously differentiable
-      exact c2R_if_holomorphic f h
+      exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
   · -- Laplace of f is zero
     intro z