From 819037fb01c2db668812119aaa28f8503c49daff Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 5 Aug 2024 15:26:28 +0200
Subject: [PATCH] =?UTF-8?q?working=E2=80=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Nevanlinna/holomorphic_primitive2.lean | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean
index 766218d..3df5fbd 100644
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@@ -535,13 +535,6 @@ theorem primitive_additivity'
     apply hf.mono
     intro x hx
     simp
-    let A := hx.1
-    simp at A
-    let B := hx.2
-    simp at B
-    calc dist x z₀
-    _ = √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) := by exact Complex.dist_eq_re_im x z₀
-    _ =
     sorry
 
   have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by