Update cauchyRiemann.lean

nevanlinna/cauchyRiemann.lean

@@ -1,15 +1,15 @@
-import Mathlib.Analysis.Calculus.Conformal.NormedSpace
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.Calculus.ContDiff.Defs
-import Mathlib.Analysis.Calculus.Deriv.Linear
-import Mathlib.Analysis.Calculus.FDeriv.Basic
-import Mathlib.Analysis.Calculus.FDeriv.Comp
-import Mathlib.Analysis.Calculus.FDeriv.Linear
-import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
+--import Mathlib.Analysis.Calculus.Conformal.NormedSpace
+--import Mathlib.Analysis.Calculus.ContDiff.Basic
+--import Mathlib.Analysis.Calculus.ContDiff.Defs
+--import Mathlib.Analysis.Calculus.Deriv.Linear
+--import Mathlib.Analysis.Calculus.FDeriv.Basic
+--import Mathlib.Analysis.Calculus.FDeriv.Comp
+--import Mathlib.Analysis.Calculus.FDeriv.Linear
+--import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 import Mathlib.Analysis.Calculus.LineDeriv.Basic
-import Mathlib.Analysis.Complex.Basic
-import Mathlib.Analysis.Complex.CauchyIntegral
-import Mathlib.Analysis.Complex.Conformal
+--import Mathlib.Analysis.Complex.Basic
+--import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.Conformal
 import Mathlib.Analysis.Complex.RealDeriv
 
 variable {z : ℂ} {f : ℂ → ℂ}
@@ -26,12 +26,9 @@ theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z)
   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₃]
@@ -54,72 +51,78 @@ theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z)
   exact CauchyRiemann₁ h
 
 theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
-  → lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I := by
+  → (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)
+   := 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₁
-  rw [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₁
-  rw [s₂]
 
-  rw [fderiv.comp, fderiv.comp]
-  simp
-  rw [CauchyRiemann₁ h]
+  constructor
+  · rw [t₂, s₂]
+    rw [fderiv.comp, fderiv.comp]
+    simp
+    rw [CauchyRiemann₁ h]
+    rw [Complex.I_mul]
+    -- DifferentiableAt ℝ Complex.im (f z)
+    exact Complex.imCLM.differentiableAt
 
-  have u₁ : ∀ w, fderiv ℝ Complex.reCLM w = Complex.reCLM := by
-    exact fun w => ContinuousLinearMap.fderiv Complex.reCLM
+    -- DifferentiableAt ℝ f z
+    exact t₀₀
 
-  --rw [u₁ (f z)]
-  have u₂ : ∀ w, fderiv ℝ Complex.imCLM w = Complex.imCLM := by
-    exact fun w => ContinuousLinearMap.fderiv Complex.imCLM
-  -- rw [u₂ (f z)]
-  rw [Complex.I_mul]
+    -- 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 ℝ 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₀₀
-
-  -- DifferentiableAt ℝ Complex.re (f z)
-  exact Complex.reCLM.differentiableAt
-
-  -- DifferentiableAt ℝ f z
-  exact t₀₀
+    -- DifferentiableAt ℝ f z
+    exact t₀₀