working

Nevanlinna/holomorphic_primitive2.lean

@@ -334,10 +334,10 @@ theorem primitive_additivity
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
   (f : ℂ  → E)
   (z₀ : ℂ)
-  (R : ℝ)
-  (hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
+  (rx ry : ℝ)
+  (hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
   (z₁ : ℂ)
-  (hz₁ : z₁ ∈ Metric.ball z₀ R)
+  (hz₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
   :
   ∀ z ∈ Metric.ball z₁ (R - dist z₁ z₀), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
   intro z hz
@@ -345,19 +345,15 @@ theorem primitive_additivity
   have H : (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) ⊆ Metric.ball z₀ R := by
     intro x hx
 
-    have a₀ : x.re ∈ Set.uIcc z₁.re z.re := by exact (Complex.mem_reProdIm.1 hx).1
-    have a₁ : x.im ∈ Set.uIcc z₀.im z₁.im := by exact (Complex.mem_reProdIm.1 hx).2
-
-
-    have A₀ : dist x.re z₀.re ≤ dist x.re z₁.re + dist z₁.re z₀.re := by apply dist_triangle
-
     have A₁ : dist x.im z₀.im ≤ dist z₁.im z₀.im := by
       apply Real.dist_right_le_of_mem_uIcc
-      rwa [Set.uIcc_comm]
+      rw [Set.uIcc_comm]
+      exact (Complex.mem_reProdIm.1 hx).2
 
     have A₂ : dist x.re z₁.re ≤ dist z.re z₁.re := by
       apply Real.dist_right_le_of_mem_uIcc
-      rwa [Set.uIcc_comm]
+      rw [Set.uIcc_comm]
+      exact (Complex.mem_reProdIm.1 hx).1
 
     have A₃ : dist z.re z₁.re < R - dist z₁ z₀ := by
       have : ∀ x₀ x₁ : ℂ, dist x₀.re x₁.re ≤ dist x₀ x₁ := by
@@ -372,8 +368,6 @@ theorem primitive_additivity
 
     simp
 
-    have B₀ : dist x z₀ ≤ dist x ⟨z₁.re, x.im⟩ + dist ⟨z₁.re, x.im⟩ z₀ := by apply dist_triangle
-
     have B₁ : dist ⟨z₁.re, x.im⟩ z₀ ≤ dist z₁ z₀ := by
       rw [Complex.dist_eq_re_im]
       rw [Complex.dist_eq_re_im]
@@ -474,6 +468,7 @@ theorem primitive_additivity
     intro w hw
     simp
 
+
     sorry --apply integrability₂ f hf
 
     sorry --apply integrability₂ f hf