From c3289f89c7ce4d9d5869d6b55542f13a4b49de3c Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 7 Aug 2024 09:21:25 +0200
Subject: [PATCH] Update holomorphic_primitive2.lean

---
 Nevanlinna/holomorphic_primitive2.lean | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index cca5e24..b2d28e6 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -303,10 +303,18 @@ theorem primitive_additivity
 
   let εx := rx - dist z₀.re z₁.re
   have hεx : εx > 0 := by
-    sorry
+    let A := hz₁.1
+    simp at A
+    dsimp [εx]
+    rw [dist_comm]
+    simpa
   let εy := ry - dist z₀.im z₁.im
   have hεy : εy > 0 := by
-    sorry
+    let A := hz₁.2
+    simp at A
+    dsimp [εy]
+    rw [dist_comm]
+    simpa
 
   use εx
   use hεx