diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index 593f65a..30e8aae 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -277,7 +277,7 @@ theorem harmonic_is_realOfHolomorphic
 
     intro x hx
     rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
-    rw [fderiv.comp]
+    rw [fderiv_comp]
     simp
     apply ContinuousLinearMap.ext
     intro w
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 3949eef..754d10f 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -202,14 +202,14 @@ theorem partialDeriv_compContLin
     left
     intro w
     left
-    rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
+    rw [fderiv_comp w (ContinuousLinearMap.differentiableAt l) (h w)]
   simp
   rfl
 
 
 theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x : E} (h : DifferentiableAt 𝕜 f x) : (partialDeriv 𝕜 v (l ∘ f)) x = (l ∘ partialDeriv 𝕜 v f) x:= by
   unfold partialDeriv
-  rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
+  rw [fderiv_comp x (ContinuousLinearMap.differentiableAt l) h]
   simp