obtain ⟨z₀, h1, h2⟩ : ∃ z₀ ∈ K, ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖ :=
  hK.exists_forall_le (nonempty_iff_ne_empty.2 h) (continuous_norm.comp_continuousOn hf1)
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
case intro.intro
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀✝ : ℂ
p : Filter ι
r : ℝ
U K : Set ℂ
hK : IsCompact K
F_conv : TendstoUniformlyOn F f p K
hf1 : ContinuousOn f K
hf2 : ∀ z ∈ K, f z ≠ 0
h : ¬K = ∅
z₀ : ℂ
h1 : z₀ ∈ K
h2 : ∀ z ∈ K, ‖f z₀‖ ≤ ‖f z‖
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0