From 9ac79470cd2b63226d0a601b2c2910ce707ef492 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 6 May 2024 17:01:10 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 39 +++++++++++++++++++--------------
 1 file changed, 22 insertions(+), 17 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 9a6c7ac..1b43551 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -52,14 +52,25 @@ lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
   · simp
 
 
-theorem holomorphic_is_harmonic (f : ℂ → ℂ) :
-  Differentiable ℂ f → Harmonic f := by
+theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
+  Harmonic f := by
+
+  -- f is real C²
+  have f_is_real_C2 : ContDiff ℝ 2 f :=
+    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+
+  -- f' is real C¹
+  have f'_is_real_C1 : ContDiff ℝ 1 (fderiv ℝ f) :=
+    (contDiff_succ_iff_fderiv.1 f_is_real_C2).right
+
+  -- f' is real differentiable
+  have f'_is_differentiable : Differentiable ℝ (fderiv ℝ f) :=
+    (contDiff_succ_iff_fderiv.1 f'_is_real_C1).left
 
-  intro h
 
   constructor
   · -- f is two times real continuously differentiable
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+    exact f_is_real_C2
 
   · -- Laplace of f is zero
     intro z
@@ -75,20 +86,14 @@ theorem holomorphic_is_harmonic (f : ℂ → ℂ) :
       intro z
       rw [CauchyRiemann₁ (h z)]
 
-    have t₂₀ : ContDiff ℝ 2 f := by exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
-    have t₀₀ : Differentiable ℝ (fun w => (fderiv ℝ f w)) := by
-      let A := (contDiff_succ_iff_fderiv.1 t₂₀).right
-      let B := (contDiff_succ_iff_fderiv.1 A).left
-      exact B
-
-    have t₀ : ∀ z, DifferentiableAt ℝ (fun w => (fderiv ℝ f w) 1) z := by
+    have t₀ : ∀ z, DifferentiableAt ℝ (fun w ↦ (fderiv ℝ f w) 1) z := by
       intro z
-      let A := t₀₀
+      let A := f'_is_differentiable
       fun_prop
 
-    have t₁ : ∀ x, (fderiv ℝ (fun w => Complex.I * (fderiv ℝ f w) 1) z) x
-      = Complex.I * ((fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) x) := by
+    have t₁ : ∀ x, (fderiv ℝ (fun w ↦ Complex.I * (fderiv ℝ f w) 1) z) x
+      = Complex.I * ((fderiv ℝ (fun w ↦ (fderiv ℝ f w) 1) z) x) := by
       intro x
       rw [fderiv_const_mul]
       simp
@@ -97,11 +102,11 @@ theorem holomorphic_is_harmonic (f : ℂ → ℂ) :
 
     have t₂ : (fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) Complex.I
       = (fderiv ℝ (fun w => (fderiv ℝ f w) Complex.I) z) 1 := by
-      let A := derivSymm f t₂₀ z 1 Complex.I
-      let B := l₂ t₂₀ z Complex.I  1
+      let A := derivSymm f f_is_real_C2 z 1 Complex.I
+      let B := l₂ f_is_real_C2 z Complex.I  1
       rw [← B]
       rw [A]
-      let C := l₂ t₂₀ z 1 Complex.I
+      let C := l₂ f_is_real_C2 z 1 Complex.I
       rw [C]
     rw [t₂]