diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index 3447e8a..393f1d4 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -97,7 +97,16 @@ theorem primitive_fderivAtBasepointZero
     have B : Metric.ball (f 0) (c / 4) ∈ nhds (f 0) := by
       apply Metric.ball_mem_nhds (f 0)
       linarith
-    exact eventually_nhds_iff.mp (continuousAt_def.1 hf (Metric.ball (f 0) (c / (4 : ℝ))) B)
+    apply eventually_nhds_iff.mp
+    apply continuousAt_def.1
+    apply Continuous.continuousAt
+    fun_prop
+
+    apply continuousAt_def.1
+    apply hf.continuousAt
+    exact Metric.ball_mem_nhds 0 hR
+    apply Metric.ball_mem_nhds (f 0)
+    simpa
 
   obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s := by
     obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by
@@ -108,13 +117,12 @@ theorem primitive_fderivAtBasepointZero
       exact Metric.isOpen_ball
       constructor
       · exact h₂s.2
-      · simp
-
-        sorry
+      · simpa
     use (2 : ℝ)⁻¹ * ε'
     constructor
     · simpa
     · intro x hx
+      apply Set.inter_subset_left
       apply h₂ε'
       simp
       calc Complex.abs x