From a5bf92552cbabc1cdc325fb23eaba2092225d9fa Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 29 Apr 2024 08:54:28 +0200 Subject: [PATCH 1/5] 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 From 77d1fd2ae4e61631c902169e56efe4ef9be9c935 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 29 Apr 2024 10:19:21 +0200 Subject: [PATCH 2/5] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- nevanlinna/cauchyRiemann.lean | 112 ++++++++++++++++++++++++++++++---- 1 file changed, 101 insertions(+), 11 deletions(-) diff --git a/nevanlinna/cauchyRiemann.lean b/nevanlinna/cauchyRiemann.lean index dd5addf..4241841 100644 --- a/nevanlinna/cauchyRiemann.lean +++ b/nevanlinna/cauchyRiemann.lean @@ -1,19 +1,22 @@ -import Mathlib.Analysis.Complex.CauchyIntegral -import Mathlib.Analysis.Complex.Basic -import Mathlib.Analysis.Calculus.LineDeriv.Basic -import Mathlib.Analysis.Calculus.ContDiff.Defs -import Mathlib.Analysis.Calculus.FDeriv.Basic -import Mathlib.Analysis.Complex.RealDeriv -import Mathlib.Analysis.Calculus.ContDiff.Basic -import Mathlib.Analysis.Calculus.Deriv.Linear -import Mathlib.Analysis.Complex.Conformal 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.RealDeriv -variable {z : ℂ} {f : ℂ → ℂ} {h : DifferentiableAt ℂ f z} +variable {z : ℂ} {f : ℂ → ℂ} -theorem CauchyRiemann₁ : fderiv ℝ f z Complex.I = Complex.I * fderiv ℝ f z 1 := by +theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z) + → (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by + intro h let A := fderiv ℂ f z have t₁ : A (Complex.I • 1) = Complex.I • (A 1) := by exact ContinuousLinearMap.map_smul_of_tower A Complex.I 1 @@ -33,3 +36,90 @@ theorem CauchyRiemann₁ : fderiv ℝ f z Complex.I = Complex.I * fderiv ℝ f z exact DifferentiableAt.fderiv_restrictScalars ℝ h rw [t₃] exact t₂c + +theorem CauchyRiemann₂ : (DifferentiableAt ℂ f z) + → lineDeriv ℝ f z Complex.I = Complex.I * lineDeriv ℝ f z 1 := by + intro h + + have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by + apply DifferentiableAt.lineDeriv_eq_fderiv + apply h.restrictScalars ℝ + rw [this] + + have : lineDeriv ℝ f z 1 = (fderiv ℝ f z) 1 := by + apply DifferentiableAt.lineDeriv_eq_fderiv + apply h.restrictScalars ℝ + rw [this] + + exact CauchyRiemann₁ h + +theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z) + → lineDeriv ℝ (Complex.reCLM ∘ f) z 1 = lineDeriv ℝ (Complex.imCLM ∘ f) z Complex.I := 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] + + have u₁ : ∀ w, fderiv ℝ Complex.reCLM w = Complex.reCLM := by + exact fun w => ContinuousLinearMap.fderiv Complex.reCLM + + --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.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₀₀ From 38eaf677f9a70d90f339edf72694f945d8585133 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 29 Apr 2024 14:19:58 +0200 Subject: [PATCH 3/5] Update cauchyRiemann.lean --- nevanlinna/cauchyRiemann.lean | 91 ++++++++++++++++++----------------- 1 file changed, 47 insertions(+), 44 deletions(-) diff --git a/nevanlinna/cauchyRiemann.lean b/nevanlinna/cauchyRiemann.lean index 4241841..6a19122 100644 --- a/nevanlinna/cauchyRiemann.lean +++ b/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₀₀ From 2d2a21be721c8728c2bf659e978373a2c1401338 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 29 Apr 2024 19:48:37 +0200 Subject: [PATCH 4/5] Update cauchyRiemann.lean --- nevanlinna/cauchyRiemann.lean | 43 ++++------------------------------- 1 file changed, 5 insertions(+), 38 deletions(-) diff --git a/nevanlinna/cauchyRiemann.lean b/nevanlinna/cauchyRiemann.lean index 6a19122..c74ff06 100644 --- a/nevanlinna/cauchyRiemann.lean +++ b/nevanlinna/cauchyRiemann.lean @@ -1,15 +1,4 @@ ---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.RealDeriv variable {z : ℂ} {f : ℂ → ℂ} @@ -17,37 +6,15 @@ variable {z : ℂ} {f : ℂ → ℂ} theorem CauchyRiemann₁ : (DifferentiableAt ℂ f z) → (fderiv ℝ f z) Complex.I = Complex.I * (fderiv ℝ f z) 1 := by intro h - let A := fderiv ℂ f z - 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 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₂c : AR Complex.I = Complex.I • (AR 1) := by - simp at t₂ - exact t₂ - have t₃ : fderiv ℝ f z = ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) := by - exact DifferentiableAt.fderiv_restrictScalars ℝ h - rw [t₃] - exact t₂c + rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + 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 - - have : lineDeriv ℝ f z Complex.I = (fderiv ℝ f z) Complex.I := by - apply DifferentiableAt.lineDeriv_eq_fderiv - apply h.restrictScalars ℝ - rw [this] - - have : lineDeriv ℝ f z 1 = (fderiv ℝ f z) 1 := by - apply DifferentiableAt.lineDeriv_eq_fderiv - apply h.restrictScalars ℝ - rw [this] - + rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)] + rw [DifferentiableAt.lineDeriv_eq_fderiv (h.restrictScalars ℝ)] exact CauchyRiemann₁ h theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z) From b2f04c1dfa59f079808d46722663294ea434b23e Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 29 Apr 2024 20:53:47 +0200 Subject: [PATCH 5/5] 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