From bcb639a5be029df2c921e429813afa5fbb65c5ae Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 17 May 2024 09:19:24 +0200
Subject: [PATCH] Fix errors

---
 Nevanlinna/cauchyRiemann.lean   |  2 +-
 Nevanlinna/complexHarmonic.lean | 22 +++++++++-------------
 2 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/Nevanlinna/cauchyRiemann.lean b/Nevanlinna/cauchyRiemann.lean
index 1272109..883749d 100644
--- a/Nevanlinna/cauchyRiemann.lean
+++ b/Nevanlinna/cauchyRiemann.lean
@@ -44,7 +44,7 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
   simp
 
 
-theorem CauchyRiemann₄ {f : ℂ → ℂ} : (Differentiable ℂ f)
+theorem CauchyRiemann₄ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} : (Differentiable ℂ f)
   → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
   intro h
   unfold partialDeriv
diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index bb5ad8f..57519f2 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -26,20 +26,20 @@ def Harmonic (f : ℂ → F) : Prop :=
   (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)
 
 
-theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G}  (h : Harmonic f) :
+theorem harmonic_comp_CLM_is_harmonic {f : ℂ → F₁} {l : F₁ →L[ℝ] G} (h : Harmonic f) :
   Harmonic (l ∘ f) := by
 
   constructor
   · -- Continuous differentiability
     apply ContDiff.comp
     exact ContinuousLinearMap.contDiff l
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+    exact h.1
   · rw [laplace_compContLin]
     simp
     intro z
     rw [h.2 z]
     simp
-    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+    exact ContDiff.restrict_scalars ℝ h.1
 
 
 theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ] G₁} :
@@ -78,21 +78,17 @@ theorem holomorphic_is_harmonic {f : ℂ → F₁} (h : Differentiable ℂ f) :
     -- This lemma says that partial derivatives commute with complex scalar
     -- multiplication. This is a consequence of partialDeriv_compContLin once we
     -- note that complex scalar multiplication is continuous ℝ-linear.
-    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
+    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → F₁, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
       intro v s g hg
 
       -- Present scalar multiplication as a continuous ℝ-linear map. This is
       -- horrible, there must be better ways to do that.
-      let sMuls : ℂ →L[ℝ] ℂ :=
+      let sMuls : F₁ →L[ℝ] F₁ :=
       {
-        toFun := fun x ↦ s * x
-        map_add' := by
-          intro x y
-          ring
-        map_smul' := by
-          intro m x
-          simp
-          ring
+        toFun := fun x ↦ s • x
+        map_add' := by exact fun x y => DistribSMul.smul_add s x y
+        map_smul' := by exact fun m x => (smul_comm ((RingHom.id ℝ) m) s x).symm
+        cont := continuous_const_smul s
       }
 
       -- Bring the goal into a form that is recognized by