MeromorphicOn.exists_nonzero_seq_divisor_support_diff_zero

lemma exists_nonzero_seq_divisor_support_diff_zero [HereditarilyLindelofSpace 𝕜]    {f : 𝕜 → E} {U : Set 𝕜} :    ∃ a : ℕ → 𝕜,      (∀ n, a n ≠ 0) ∧ (MeromorphicOn.divisor f U).support \ {0} ⊆ Set.range a := by  classical  set s : Set 𝕜 := (MeromorphicOn.divisor f U).support \ {0}  by_cases hs : s.Nonempty  · have hs_count : s.Countable := by      have hsup : (MeromorphicOn.divisor f U).support.Countable :=        MeromorphicOn.divisor_support_countable (f := f) (U := U)      refine hsup.mono ?_      intro x hx      exact hx.1    rcases hs_count.exists_eq_range hs with ⟨a, ha⟩    refine ⟨a, ?_, ?_⟩    · intro n      have : a n ∈ s := by        simp [ha]      exact fun h0 => this.2 (by simpa [Set.mem_singleton_iff] using h0)    · simp [ha]  · refine ⟨fun _ => (1 : 𝕜), ?_, ?_⟩    · intro _; simp    · have : s = ∅ := Set.not_nonempty_iff_eq_empty.1 hs      simp [this]