Complex.hasProdLocallyUniformlyOn_weierstrassFactor_div

lemma hasProdLocallyUniformlyOn_weierstrassFactor_div {s : Set ℂ} (hs : IsOpen s)    {m : ℕ → ℕ} {a : ℕ → ℂ}    (hsmall : ∀ R ≥ 0, ∀ᶠ n in Filter.atTop, R ≤ ‖a n‖ / 2)    (hsumm : ∀ R ≥ 0, Summable (fun n : ℕ ↦ 4 * R ^ (m n + 1) / ‖a n‖ ^ (m n + 1))) :    HasProdLocallyUniformlyOn (fun n z ↦ weierstrassFactor (m n) (z / a n))      (fun z ↦ ∏' n, weierstrassFactor (m n) (z / a n)) s := by  apply hasProdLocallyUniformlyOn_of_forall_compact hs  intro K hKs hK  obtain ⟨R, hR⟩ : ∃ R, ∀ z ∈ K, ‖z‖ ≤ R := by    by_cases hKe : K.Nonempty    · obtain ⟨z, hzK, hzmax⟩ := hK.exists_isMaxOn hKe continuous_norm.continuousOn      exact ⟨‖z‖, fun w hw ↦ (isMaxOn_iff.mp hzmax) w hw⟩    · exact ⟨0, fun z hz ↦ False.elim <| hKe ⟨z, hz⟩⟩  let R' := max R 0  have hR'0 : 0 ≤ R' := le_max_right _ _  have hR' : ∀ z ∈ K, ‖z‖ ≤ R' := by    intro z hz    exact (hR z hz).trans (le_max_left _ _)  exact hasProdUniformlyOn_weierstrassFactor_div_of_bound hK hR'    (hsmall R' hR'0) (hsumm R' hR'0)