Complex.Hadamard.no_zero_on_sphere_of_norm_image_avoid

lemma no_zero_on_sphere_of_norm_image_avoid    {f : ℂ → ℂ} (hentire : Differentiable ℂ f) (hnot : ∃ z : ℂ, f z ≠ 0)    {B r : ℝ} (hrpos : 0 < r) (hr_le_B : r ≤ B)    (smallSet : Set (divisorZeroIndex₀ f (Set.univ : Set ℂ))) (hsmall_fin : smallSet.Finite)    (hsmallSet :      smallSet = {p : divisorZeroIndex₀ f (Set.univ : Set ℂ) | ‖divisorZeroIndex₀_val p‖ ≤ B})    (hr_not_bad :      let small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := hsmall_fin.toFinset      let a : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ := fun p => ‖divisorZeroIndex₀_val p‖      r ∉ small.image a) :    ∀ u : ℂ, ‖u‖ = r → f u ≠ 0 := by  classical  let small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := hsmall_fin.toFinset  let a : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ := fun p => ‖divisorZeroIndex₀_val p‖  let bad : Finset ℝ := small.image a  have hr_not_bad' : r ∉ bad := by    simpa [bad, small, a] using hr_not_bad  have hr_not :      ∀ p : divisorZeroIndex₀ f (Set.univ : Set ℂ),        ‖divisorZeroIndex₀_val p‖ ≤ B → r ≠ ‖divisorZeroIndex₀_val p‖ := by    intro p hpB hEq    have hp_small : p ∈ small := by      have hp_mem : p ∈ smallSet := by        simpa [hsmallSet] using hpB      simpa [small] using (hsmall_fin.mem_toFinset.2 hp_mem)    have : r ∈ bad := Finset.mem_image.2 ⟨p, hp_small, by simpa [a] using hEq.symm⟩    exact (hr_not_bad' this).elim  exact no_zero_on_sphere_of_forall_val_norm_ne (f := f) hentire hnot    (B := B) (r := r) hrpos hr_le_B hr_not