diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 691a92e..506339a 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -39,9 +39,9 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
   · -- Laplace of f is zero
     unfold Complex.laplace
     rw [CauchyRiemann₄ h]
-    rw [partialDeriv_smul fI_is_real_differentiable]
+    rw [partialDeriv_smul₂ fI_is_real_differentiable]
     rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
     rw [CauchyRiemann₄ h]
-    rw [partialDeriv_smul fI_is_real_differentiable]
+    rw [partialDeriv_smul₂ fI_is_real_differentiable]
     rw [← smul_assoc]
     simp
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 7e5862c..20be9da 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -14,7 +14,24 @@ noncomputable def Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) :=
   fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v))
 
 
-theorem partialDeriv_smul {f : ℂ → ℂ} {a v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
+
+theorem partialDeriv_smul₁ {f : ℂ → ℂ} {a : ℝ} {v : ℂ} : Real.partialDeriv (a • v) f = a • Real.partialDeriv v f := by
+  unfold Real.partialDeriv
+  conv =>
+    left
+    intro w
+    rw [map_smul]
+
+
+theorem partialDeriv_add₁ {f : ℂ → ℂ} {v₁ v₂ : ℂ} : Real.partialDeriv (v₁ + v₂) f = (Real.partialDeriv v₁ f) + (Real.partialDeriv v₂ f) := by
+  unfold Real.partialDeriv
+  conv =>
+    left
+    intro w
+    rw [map_add]
+
+
+theorem partialDeriv_smul₂ {f : ℂ → ℂ} {a v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
   unfold Real.partialDeriv
 
   have : a • f = fun y ↦ a • f y := by rfl
@@ -26,7 +43,7 @@ theorem partialDeriv_smul {f : ℂ → ℂ} {a v : ℂ} (h : Differentiable ℝ
     rw [fderiv_const_smul (h w)]
 
 
-theorem partialDeriv_add {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differentiable ℝ f₁)  (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by
+theorem partialDeriv_add₂ {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differentiable ℝ f₁)  (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by
   unfold Real.partialDeriv
 
   have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
@@ -38,7 +55,7 @@ theorem partialDeriv_add {f₁ f₂ : ℂ → ℂ} {v : ℂ} (h₁ : Differentia
     rw [fderiv_add (h₁ w) (h₂ w)]
 
 
-theorem partialDeriv_compLin {f : ℂ → ℂ} {l : ℂ →L[ℝ] ℂ} {v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by
+theorem partialDeriv_compContLin {f : ℂ → ℂ} {l : ℂ →L[ℝ] ℂ} {v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by
   unfold Real.partialDeriv
 
   conv =>