From 7893050455b8ab1b0c9ae49d8c26835411c96a06 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 12 Nov 2024 13:14:11 +0100
Subject: [PATCH] Update along with mathlib

---
 Nevanlinna/holomorphic_examples.lean | 2 +-
 Nevanlinna/partialDeriv.lean         | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

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