diff --git a/Nevanlinna/holomorphic_examples.lean b/Nevanlinna/holomorphic_examples.lean
index 30e8aae..67553d5 100644
--- a/Nevanlinna/holomorphic_examples.lean
+++ b/Nevanlinna/holomorphic_examples.lean
@@ -204,7 +204,7 @@ theorem harmonic_is_realOfHolomorphic
 
       --DifferentiableAt ℝ (partialDeriv ℝ _ f)
       repeat
-        apply ContDiffAt.differentiableAt
+        apply ContDiffAt.differentiableAt (n := 1)
         apply partialDeriv_contDiffAt ℝ (hf x hx).1
         apply le_rfl
 
diff --git a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
index 803b68f..22cb1b1 100644
--- a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
+++ b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
@@ -20,7 +20,7 @@ theorem jensen_case_R_eq_one
 
   have h₁U : IsConnected (Metric.closedBall (0 : ℂ) 1) := by
     constructor
-    · exact Set.Nonempty.of_subtype
+    · refine Metric.nonempty_closedBall.mpr (by simp)
     · exact (convex_closedBall (0 : ℂ) 1).isPreconnected
 
   have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=