From a5bf92552cbabc1cdc325fb23eaba2092225d9fa Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 29 Apr 2024 08:54:28 +0200
Subject: [PATCH] Update cauchyRiemann.lean

---
 nevanlinna/cauchyRiemann.lean | 51 +++++++++++++----------------------
 1 file changed, 18 insertions(+), 33 deletions(-)

diff --git a/nevanlinna/cauchyRiemann.lean b/nevanlinna/cauchyRiemann.lean
index 5d649ed..dd5addf 100644
--- a/nevanlinna/cauchyRiemann.lean
+++ b/nevanlinna/cauchyRiemann.lean
@@ -11,40 +11,25 @@ import Mathlib.Analysis.Calculus.Conformal.NormedSpace
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 
-variable {z : ℂ} {f : ℂ → ℂ}
-
-example (h : DifferentiableAt ℂ f z) : f z = 0 := by
+variable {z : ℂ} {f : ℂ → ℂ} {h : DifferentiableAt ℂ f z}
 
+theorem CauchyRiemann₁ : fderiv ℝ f z Complex.I = Complex.I * fderiv ℝ f z 1 := by
   let A := fderiv ℂ f z
-  let B := fderiv ℝ f
-
-  let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
-  let D := ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)
-  let E := D 1
-  let F := D Complex.I
-
-  have : A (Complex.I • 1) = Complex.I • (A 1) := by
+  have t₁ : A (Complex.I • 1) = Complex.I • (A 1) := by
     exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1
-
   let AR := (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
-  have : AR (Complex.I • 1) = Complex.I • (AR 1) := by
-    exact this
-
-  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
-  have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by
-    apply DifferentiableAt.lineDeriv_eq_fderiv
-    apply h.restrictScalars ℝ
-
-  have : D Complex.I = Complex.I * (D 1) := by
-    -- x
-
-    sorry
-
-  have : HasFDerivAt f A z := by
-    exact DifferentiableAt.hasFDerivAt h
-
-  have : HasFDerivAt f (B z) z := by
-    sorry
-
-
-  sorry
+  have t₂ : AR (Complex.I • 1) = Complex.I • (AR 1) := by
+    exact t₁
+  have t₂a : Complex.I * (AR 1) = Complex.I • (AR 1) := by
+    exact rfl
+  rw [← t₂a] at t₂
+  have t₂b : Complex.I • 1 = Complex.I := by
+    simp
+  have t₂c : AR Complex.I = Complex.I • (AR 1) := by
+    simp at t₂
+    exact t₂
+  let C : HasFDerivAt f (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) z := h.hasFDerivAt.restrictScalars ℝ
+  have t₃ : fderiv ℝ f z = ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) := by
+    exact DifferentiableAt.fderiv_restrictScalars ℝ h
+  rw [t₃]
+  exact t₂c