working…

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