working

Nevanlinna/holomorphic_primitive2.lean

@@ -515,9 +515,9 @@ theorem primitive_additivity'
   :
   primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
 
-  let d := fun ε ↦ √((z₁.re - z₀.re + ε) ^ 2 + (z₁.im - z₀.im + ε) ^ 2)
+  let d := fun ε ↦ √((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
   have h₀d : Continuous d := by continuity
-  have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((z₁.re - z₀.re + ε) ^ 2 + (z₁.im - z₀.im + ε) ^ 2)
+  have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
 
   obtain ⟨ε, h₀ε, h₁ε⟩ : ∃ ε > 0, d ε < R := by
     let Omega := d⁻¹' Metric.ball 0 R
@@ -525,6 +525,11 @@ theorem primitive_additivity'
     have lem₀Ω : IsOpen Omega := IsOpen.preimage h₀d Metric.isOpen_ball
     have lem₁Ω : 0 ∈ Omega := by
       dsimp [Omega, d]; simp
+      have : dist z₁.re z₀.re = |z₁.re - z₀.re| := by exact rfl
+      rw [this]
+      have : dist z₁.im z₀.im = |z₁.im - z₀.im| := by exact rfl
+      rw [this]
+      simp
       rw [← Complex.dist_eq_re_im]; simp
       exact hz₁
     obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
@@ -570,13 +575,17 @@ theorem primitive_additivity'
     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
-      sorry
-    have t₁ : √( rx ^ 2 + ry ^ 2) = d ε := by
-      sorry
+      rw [Real.sqrt_lt_sqrt_iff]
+      apply add_lt_add
+      · dsimp [rx]
+
+        sorry
+      · sorry
 
     calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2)
-    _ < √( rx ^ 2 + ry ^ 2) := by exact t₀
-    _ = d ε := by exact t₁
+    _ < √( rx ^ 2 + ry ^ 2) := by
+      exact t₀
+    _ = d ε := by dsimp [d, rx, ry]
     _ < R := by exact h₁ε
 
   have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by