Update holomorphic_zero.lean

Nevanlinna/holomorphic_zero.lean

@@ -115,7 +115,7 @@ theorem zeroDivisor_support_iff
     assumption
 
 
-example
+theorem topOnPreconnected
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hU : IsPreconnected U)
@@ -132,6 +132,40 @@ example
   tauto
 
 
+theorem supportZeroSet
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hU : IsPreconnected U)
+  (h₁f : AnalyticOn ℂ f U)
+  (h₂f : ∃ z ∈ U, f z ≠ 0) :
+  U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by
+
+  ext x
+  constructor
+  · intro hx
+    constructor
+    · exact hx.1
+    exact zeroDivisor_zeroSet hx.2
+  · simp
+    intro h₁x h₂x
+    constructor
+    · exact h₁x
+    · let A := zeroDivisor_support_iff (f := f) (z₀ := x)
+      simp at A
+      rw [A]
+      constructor
+      · exact h₂x
+      · constructor
+        · exact h₁f x h₁x
+        · have B := AnalyticAt.order_eq_nat_iff (h₁f x h₁x) (zeroDivisor f x)
+          simp at B
+          rw [← B]
+          dsimp [zeroDivisor]
+          simp [h₁f x h₁x]
+          refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a)
+          exact topOnPreconnected hU h₁f h₂f h₁x
+
+
 theorem discreteZeros
   {f : ℂ → ℂ} :
   DiscreteTopology (Function.support (zeroDivisor f)) := by