Complex.Hadamard.analyticOrderNatAt_divisorCanonicalProduct_eq_fiber_card

theorem analyticOrderNatAt_divisorCanonicalProduct_eq_fiber_card    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) :    analyticOrderNatAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) z₀ =      (divisorZeroIndex₀_fiberFinset (f := f) z₀).card := by  set k : ℕ := (divisorZeroIndex₀_fiberFinset (f := f) z₀).card  let F : ℂ → ℂ := divisorCanonicalProduct m f (Set.univ : Set ℂ)  let q0 : ℂ → ℂ := fun z => F z / (z - z₀) ^ k  rcases exists_analyticAt_divisorCanonicalProduct_quotient      (m := m) (f := f) (h_sum := h_sum) (z₀ := z₀) with    ⟨q, hqA, hq_self, hq_ne⟩  have hdiff_univ : DifferentiableOn ℂ F (Set.univ : Set ℂ) :=    differentiableOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum  have han : AnalyticAt ℂ F z₀ := by    refine (Complex.analyticAt_iff_eventually_differentiableAt).2 ?_    refine Filter.Eventually.of_forall ?_    intro z    have : DifferentiableWithinAt ℂ F (Set.univ : Set ℂ) z := hdiff_univ z (by simp)    exact this.differentiableAt (by simp)  rcases      exists_ball_eq_divisorCanonicalProduct_div_pow_eq (m := m) (f := f) (h_sum := h_sum)      (z₀ := z₀)    with ⟨ε, hε, u, huA, hu0, hEq⟩  let g : ℂ → ℂ := fun z => (divisorComplementCanonicalProduct m f z₀ z) * u z  have hcompDiff : DifferentiableOn ℂ (divisorComplementCanonicalProduct m f z₀)      (Set.univ : Set ℂ) :=    differentiableOn_divisorComplementCanonicalProduct_univ (m := m) (f := f) (z₀ := z₀) h_sum  have hcompCont : ContinuousAt (divisorComplementCanonicalProduct m f z₀) z₀ :=    (hcompDiff z₀ (by simp)).differentiableAt (by simp) |>.continuousAt  have hgCont : ContinuousAt g z₀ := (hcompCont.mul huA.continuousAt)  have hg0 : g z₀ ≠ 0 := by    have hcomp0 : divisorComplementCanonicalProduct m f z₀ z₀ ≠ 0 :=      divisorComplementCanonicalProduct_ne_zero_at (m := m) (f := f) (z₀ := z₀) h_sum    exact mul_ne_zero hcomp0 hu0  have hne_mem : ∀ᶠ z in 𝓝[≠] z₀, z ∈ (({z₀} : Set ℂ)ᶜ) :=    Filter.eventually_of_mem      (self_mem_nhdsWithin : (({z₀} : Set ℂ)ᶜ) ∈ 𝓝[≠] z₀) (fun _ hz => hz)  have hne : ∀ᶠ z in 𝓝[≠] z₀, z ≠ z₀ := by    filter_upwards [hne_mem] with z hz    simpa [Set.mem_compl_singleton_iff] using hz  have ht_q0 : Tendsto q0 (𝓝[≠] z₀) (𝓝 (g z₀)) := by    have hball : ∀ᶠ z in 𝓝[≠] z₀, z ∈ Metric.ball z₀ ε :=      Filter.eventually_of_mem        (mem_nhdsWithin_of_mem_nhds (Metric.ball_mem_nhds z₀ hε)) (fun _ hz => hz)    have heq : q0 =ᶠ[𝓝[≠] z₀] g := by      filter_upwards [hball, hne] with z hz hzne      have hq := hEq z hz hzne      simpa [q0, F, k, g, smul_eq_mul] using hq    exact (hgCont.continuousWithinAt.tendsto.congr' heq.symm)  have hlim : limUnder (𝓝[≠] z₀) q0 = g z₀ := ht_q0.limUnder_eq  have hq0 : q z₀ ≠ 0 := by    have hq_self' : q z₀ = limUnder (𝓝[≠] z₀) q0 := by      simpa [q0, F, k] using hq_self    have : q z₀ = g z₀ := hq_self'.trans hlim    exact this.symm ▸ hg0  have heq_punct : (fun z : ℂ => F z) =ᶠ[𝓝[≠] z₀] fun z : ℂ => (z - z₀) ^ k • q z := by    filter_upwards [hne] with z hz    have hzpow : (z - z₀) ^ k ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hz)    have hq : q z = q0 z := by simpa [q0, F, k] using hq_ne z hz    have hmul : (z - z₀) ^ k * q0 z = F z := by      calc        (z - z₀) ^ k * q0 z            = (((z - z₀) ^ k) * F z) / ((z - z₀) ^ k) := by                simp [q0, div_eq_mul_inv, mul_assoc]        _ = F z := by              simpa [mul_assoc] using (mul_div_cancel_left₀ (F z) hzpow)    have : F z = (z - z₀) ^ k * q z := by      calc        F z = (z - z₀) ^ k * q0 z := hmul.symm        _ = (z - z₀) ^ k * q z := by simp [hq]    simpa [smul_eq_mul] using this  have hcontF : ContinuousAt F z₀ :=    (hdiff_univ z₀ (by simp)).differentiableAt (by simp) |>.continuousAt  have hcontq : ContinuousAt q z₀ := hqA.continuousAt  have h_at_z0 : F z₀ = (z₀ - z₀) ^ k • q z₀ := by    have ht1 : Tendsto F (𝓝[≠] z₀) (𝓝 (F z₀)) := hcontF.continuousWithinAt.tendsto    have hpow :        Tendsto (fun z : ℂ => (z - z₀) ^ k) (𝓝[≠] z₀) (𝓝 ((z₀ - z₀) ^ k)) :=      ((continuousAt_id.sub continuousAt_const).pow k).continuousWithinAt.tendsto    have ht2 :        Tendsto (fun z : ℂ => (z - z₀) ^ k • q z) (𝓝[≠] z₀)          (𝓝 ((z₀ - z₀) ^ k • q z₀)) :=      hpow.mul (hcontq.continuousWithinAt.tendsto)    have ht2' : Tendsto F (𝓝[≠] z₀) (𝓝 ((z₀ - z₀) ^ k • q z₀)) :=      ht2.congr' heq_punct.symm    exact tendsto_nhds_unique ht1 ht2'  have hfac : ∀ᶠ z in 𝓝 z₀, F z = (z - z₀) ^ k • q z := by    have hball1 : Metric.ball z₀ 1 ∈ 𝓝 z₀ := Metric.ball_mem_nhds z₀ (by norm_num)    have hball1' : ∀ᶠ z in 𝓝 z₀, z ∈ Metric.ball z₀ 1 :=      Filter.eventually_of_mem hball1 (fun _ hz => hz)    filter_upwards [hball1'] with z _hz    by_cases hz0 : z = z₀    · subst hz0      simpa using h_at_z0    · have hzpow : (z - z₀) ^ k ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hz0)      have hq : q z = q0 z := by simpa [q0, F, k] using hq_ne z hz0      have hmul : (z - z₀) ^ k * q0 z = F z := by        calc          (z - z₀) ^ k * q0 z              = (((z - z₀) ^ k) * F z) / ((z - z₀) ^ k) := by                  simp [q0, div_eq_mul_inv, mul_assoc]          _ = F z := by                simpa [mul_assoc] using (mul_div_cancel_left₀ (F z) hzpow)      have : F z = (z - z₀) ^ k * q z := by        calc          F z = (z - z₀) ^ k * q0 z := hmul.symm          _ = (z - z₀) ^ k * q z := by simp [hq]      simpa [smul_eq_mul] using this  have hk' : analyticOrderAt F z₀ = k :=    (han.analyticOrderAt_eq_natCast (n := k)).2 ⟨q, hqA, hq0, hfac⟩  have hkNat : analyticOrderNatAt F z₀ = k := by    simp [analyticOrderNatAt, hk']  simpa [F, k] using hkNat