by_cases h : K = ∅
ι : 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
⊢ ∀ᶠ (n : ι) in p, ∀ z ∈ K, F n z ≠ 0
case pos
ι : 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 neg
ι : 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