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

---
 nevanlinna/cauchyRiemann.lean | 79 ++++++-----------------------------
 1 file changed, 12 insertions(+), 67 deletions(-)

diff --git a/nevanlinna/cauchyRiemann.lean b/nevanlinna/cauchyRiemann.lean
index c74ff06..ba521d0 100644
--- a/nevanlinna/cauchyRiemann.lean
+++ b/nevanlinna/cauchyRiemann.lean
@@ -22,74 +22,19 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
     ∧ (lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = -lineDeriv ℝ (Complex.imCLM ∘ f) z 1)
    := by
 
-  -- Proof starts here
   intro h
 
-  have t₀₀ : DifferentiableAt ℝ f z := by
-    exact h.restrictScalars ℝ
-  have t₀₁ : DifferentiableAt ℝ Complex.reCLM (f z) := by
-    have : ∀ w, DifferentiableAt ℝ Complex.reCLM w := by
-      intro w
-      refine Differentiable.differentiableAt ?h
-      exact ContinuousLinearMap.differentiable (Complex.reCLM : ℂ →L[ℝ] ℝ)
-    exact this (f z)
-  have t₁ : DifferentiableAt ℝ (Complex.reCLM ∘ f) z := by
-    apply t₀₁.comp
-    exact t₀₀
-  have t₂ : lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = (fderiv ℝ (Complex.reCLM ∘ f) z) 1 := by
-    apply DifferentiableAt.lineDeriv_eq_fderiv
-    exact t₁
-  have s₀₀ : DifferentiableAt ℝ f z := by
-    exact h.restrictScalars ℝ
-  have s₀₁ : DifferentiableAt ℝ Complex.imCLM (f z) := by
-    have : ∀ w, DifferentiableAt ℝ Complex.imCLM w := by
-      intro w
-      apply Differentiable.differentiableAt
-      exact ContinuousLinearMap.differentiable (Complex.imCLM : ℂ →L[ℝ] ℝ)
-    exact this (f z)
-  have s₁ : DifferentiableAt ℝ (Complex.im ∘ f) z := by
-    apply s₀₁.comp
-    exact s₀₀
-  have s₂ : lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I = (fderiv ℝ (Complex.imCLM ∘ f) z) Complex.I := by
-    apply DifferentiableAt.lineDeriv_eq_fderiv
-    exact s₁
-
-  constructor
-  · rw [t₂, s₂]
-    rw [fderiv.comp, fderiv.comp]
+  have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
+    intro w l
+    rw [DifferentiableAt.lineDeriv_eq_fderiv]
+    rw [fderiv.comp]
     simp
-    rw [CauchyRiemann₁ h]
-    rw [Complex.I_mul]
-    -- DifferentiableAt ℝ Complex.im (f z)
-    exact Complex.imCLM.differentiableAt
+    fun_prop
+    exact h.restrictScalars ℝ  
+    apply (ContinuousLinearMap.differentiableAt l).comp
+    exact h.restrictScalars ℝ
 
-    -- DifferentiableAt ℝ f z
-    exact t₀₀
-
-    -- DifferentiableAt ℝ Complex.re (f z)
-    exact Complex.reCLM.differentiableAt
-
-    -- DifferentiableAt ℝ f z
-    exact t₀₀
-  · have r₂ : lineDeriv ℝ (Complex.reCLM ∘ f) z Complex.I = (fderiv ℝ (Complex.reCLM ∘ f) z) Complex.I := by
-      apply DifferentiableAt.lineDeriv_eq_fderiv
-      exact t₁
-    have p₂ : lineDeriv ℝ (Complex.imCLM ∘ f) z 1 = (fderiv ℝ (Complex.imCLM ∘ f) z) 1 := by
-      apply DifferentiableAt.lineDeriv_eq_fderiv
-      exact s₁
-    rw [r₂, p₂]
-    rw [fderiv.comp, fderiv.comp]
-    simp
-    rw [CauchyRiemann₁ h]
-    rw [Complex.I_mul]
-    -- DifferentiableAt ℝ Complex.im (f z)
-    exact Complex.imCLM.differentiableAt
-
-    -- DifferentiableAt ℝ f z
-    exact t₀₀
-
-    -- DifferentiableAt ℝ Complex.re (f z)
-    exact Complex.reCLM.differentiableAt
-
-    -- DifferentiableAt ℝ f z
-    exact t₀₀
+  repeat
+    rw [ContinuousLinearMap.comp_lineDeriv]
+  rw [CauchyRiemann₁ h, Complex.I_mul]
+  simp