refine (isCompact_𝓜 hU).of_isClosed_subset ?_ (λ _ hf => hf.1)
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsCompact (𝓙 U)
ι : Type u_1
l : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
⊢ IsClosed (𝓙 U)