Complex.Hadamard.analyticOrderAt_partialProduct_eq_fiberCard_of_subset

theorem analyticOrderAt_partialProduct_eq_fiberCard_of_subset    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)))    (hs : divisorZeroIndex₀_fiberFinset (f := f) z₀ ⊆ s) :    analyticOrderAt        (fun z : ℂ => ∏ p ∈ s, weierstrassFactor m (z / divisorZeroIndex₀_val p))        z₀ = ((divisorZeroIndex₀_fiberFinset (f := f) z₀).card : ℕ∞) := by  have h :=    analyticOrderAt_finset_prod_weierstrassFactor_divisorZeroIndex₀      (m := m) (f := f) (s := s) (z₀ := z₀)  have hfilter :      s.filter (fun p => divisorZeroIndex₀_val p = z₀) =        divisorZeroIndex₀_fiberFinset (f := f) z₀ := by    ext p    constructor    · intro hp'      have hpv : divisorZeroIndex₀_val p = z₀ := (Finset.mem_filter.mp hp').2      simpa [mem_divisorZeroIndex₀_fiberFinset] using hpv    · intro hp_fiber      have hpv : divisorZeroIndex₀_val p = z₀ :=        (mem_divisorZeroIndex₀_fiberFinset (f := f) (z₀ := z₀) p).1 hp_fiber      have hps : p ∈ s := hs (by simpa [mem_divisorZeroIndex₀_fiberFinset] using hpv)      exact Finset.mem_filter.2 ⟨hps, hpv⟩  simpa [hfilter] using h