From c44f4fe3b0c5ff69655680e4c249faa527f4566c Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 6 May 2024 09:01:43 +0200
Subject: [PATCH] Cleanup

---
 Nevanlinna/cauchyRiemann.lean   | 3 +++
 Nevanlinna/complexHarmonic.lean | 6 +++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/cauchyRiemann.lean b/Nevanlinna/cauchyRiemann.lean
index 68ea2c9..755fc68 100644
--- a/Nevanlinna/cauchyRiemann.lean
+++ b/Nevanlinna/cauchyRiemann.lean
@@ -3,6 +3,7 @@ import Mathlib.Analysis.Complex.RealDeriv
 
 variable {z : ℂ} {f : ℂ → ℂ}
 
+
 theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
   → (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by
   intro h
@@ -10,6 +11,7 @@ theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
   nth_rewrite 1 [← mul_one Complex.I]
   exact ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1
 
+
 theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
   → lineDeriv ℝ f z Complex.I = Complex.I * lineDeriv ℝ f z 1 := by
   intro h
@@ -17,6 +19,7 @@ theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
   rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)]
   exact CauchyRiemann₁ h
 
+
 theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
   → (lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I)
     ∧ (lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = -lineDeriv ℝ (Complex.imCLM ∘ f) z 1)
diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 5a907c8..e75bea7 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -20,7 +20,6 @@ noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
 def Harmonic (f : ℂ → ℂ) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
-#check second_derivative_symmetric
 
 lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℝ × ℝ, 0 = 1 := by
   intro z a b
@@ -61,13 +60,14 @@ lemma derivSymm (f : ℂ → ℂ) (h : Differentiable ℝ f) :
   dsimp [f'', f'] at A
   apply A
 
-theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
+
+theorem holomorphic_is_harmonic (f : ℂ → ℂ) :
   Differentiable ℂ f → Harmonic f := by
 
   intro h
 
   constructor
-  · -- Complex.reCLM ∘ f is two times real continuously differentiable
+  · -- f is two times real continuously differentiable
     exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
   · -- Laplace of f is zero