Update analyticOn_zeroSet.lean

Nevanlinna/analyticOn_zeroSet.lean

@@ -100,89 +100,44 @@ theorem AnalyticOn.order_eq_nat_iff'
   {U : Set ℂ}
   {A : Finset U}
   (hf : AnalyticOn ℂ f U)
-  (n : A → ℕ) :
-  ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a, g a ≠ 0) ∧ ∀ z, f z = (∏ a, (z - a) ^ (n a)) • g z := by
+  (n : ℂ → ℕ) :
+  (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
 
-  apply Finset.induction
+  apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
 
-  let a : A := by sorry
-  let b : ℂ := by sorry
-  let u : U := by sorry
+  -- case empty
+  simp
+  use f
+  simp
+  exact hf
 
-  let X := n a
-  have : a = (3 : ℂ) := by sorry
-  have : b ∈ ↑A := by sorry
-  have : ↑a ∈ U := by exact Subtype.coe_prop a.val
+  -- case insert
+  intro b₀ B hb iHyp
+  intro hBinsert
+  obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha))
 
-  let Y := ∀ a : A, (hf a (Subtype.coe_prop a.val)).order = n a
+  have : (h₁g₀ b₀ b₀.2).order = n b₀ := by sorry
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this
 
-  --∀ a : A, (hf (ha a)).order = ↑(n a) →
-
-  intro hn
-  obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn
-
-  -- Define a candidate function
-  let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n
-
-  -- Describe g near z₀
-  have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by
-    rw [eventually_nhds_iff]
-    obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc
-    use t
-    constructor
-    · intro y h₁y
-      by_cases h₂y : y = z₀
-      · dsimp [g]; simp [h₂y]
-      · dsimp [g]; simp [h₂y]
-        rw [div_eq_iff_mul_eq, eq_comm, mul_comm]
-        exact h₁t y h₁y
-        norm_num
-        rw [sub_eq_zero]
-        tauto
-    · constructor
-      · assumption
-      · assumption
-
-  -- Describe g near points z₁ different from z₀
-  have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by
-    intro hz₁
-    rw [eventually_nhds_iff]
-    use {z₀}ᶜ
-    constructor
-    · intro y hy
-      simp at hy
-      simp [g, hy]
-    · exact ⟨isOpen_compl_singleton, hz₁⟩
-
-  -- Use g and show that it has all required properties
-  use g
+  use g₁
   constructor
-  · -- AnalyticOn ℂ g U
-    intro z h₁z
-    by_cases h₂z : z = z₀
-    · rw [h₂z]
-      apply AnalyticAt.congr h₁gloc
-      exact Filter.EventuallyEq.symm g_near_z₀
-    · simp_rw [eq_comm] at g_near_z₁
-      apply AnalyticAt.congr _ (g_near_z₁ h₂z)
-      apply AnalyticAt.div
-      exact hf z h₁z
-      apply AnalyticAt.pow
-      apply AnalyticAt.sub
-      apply analyticAt_id
-      apply analyticAt_const
-      simp
-      rw [sub_eq_zero]
-      tauto
+  · exact h₁g₁
   · constructor
-    · simp [g]; tauto
+    · intro a h₁a
+      by_cases h₂a : a = b₀
+      · rwa [h₂a]
+      · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a
+        let B' := h₃g₁ a
+        let C' := h₂g₀ a A'
+        rw [B'] at C'
+        exact right_ne_zero_of_smul C'
     · intro z
-      by_cases h₂z : z = z₀
-      · rw [h₂z, g_near_z₀.self_of_nhds]
-        exact h₃gloc.self_of_nhds
-      · rw [(g_near_z₁ h₂z).self_of_nhds]
-        simp [h₂z]
-        rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel]
-        simp; norm_num
-        rw [sub_eq_zero]
-        tauto
+      let A' := h₃g₀ z
+      rw [h₃g₁ z] at A'
+      rw [A']
+      rw [← smul_assoc]
+      congr
+      simp
+      rw [Finset.prod_insert]
+      ring
+      exact hb