Update holomorphic_primitive2.lean

Nevanlinna/holomorphic_primitive2.lean

@@ -533,7 +533,6 @@ theorem primitive_additivity'
       rw [← Complex.dist_eq_re_im]; simp
       exact hz₁
     obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
-    have h'₁ε : 0 < ε := by exact h₁ε
 
     let ε' := (2 : ℝ)⁻¹ * ε
 
@@ -571,20 +570,28 @@ theorem primitive_additivity'
     simp
     rw [Complex.dist_eq_re_im]
 
-    have : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
-    have : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
-
-    have t₀ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
+    have t₀ : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
+    have t₁ : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
+    have t₂ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
       rw [Real.sqrt_lt_sqrt_iff]
       apply add_lt_add
-      · dsimp [rx]
-
-        sorry
-      · sorry
+      · rw [sq_lt_sq]
+        dsimp [dist] at t₀
+        nth_rw 2 [abs_of_nonneg]
+        assumption
+        apply add_nonneg dist_nonneg (le_of_lt h₀ε)
+      · rw [sq_lt_sq]
+        dsimp [dist] at t₁
+        nth_rw 2 [abs_of_nonneg]
+        assumption
+        apply add_nonneg dist_nonneg (le_of_lt h₀ε)
+      apply add_nonneg
+      exact sq_nonneg (x.re - z₀.re)
+      exact sq_nonneg (x.im - z₀.im)
 
     calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2)
     _ < √( rx ^ 2 + ry ^ 2) := by
-      exact t₀
+      exact t₂
     _ = d ε := by dsimp [d, rx, ry]
     _ < R := by exact h₁ε