simp [h] at hn h2
case h
ι : 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
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
hn : dist (f z) (F n z) < ‖f z₀‖
h2 : ‖f z₀‖ ≤ ‖f z‖
⊢ False
case h
ι : 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
h3 : ∀ᶠ (n : ι) in p, ∀ x ∈ K, dist (f x) (F n x) < ‖f z₀‖
n : ι
z : ℂ
hz : z ∈ K
h : F n z = 0
h2 : Complex.abs (f z₀) ≤ Complex.abs (f z)
hn : Complex.abs (f z) < Complex.abs (f z₀)
⊢ False