refine ⟨(IsClosed_𝓜 hU).mem_of_tendsto h1 (h2.mono (λ _ h => h.1)), ?_⟩
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ f ∈ 𝓙 U
case intro
ι : Type u_1
l✝ : Filter ι
U : Set ℂ
z₀ : ℂ
inst✝ : good_domain U
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓙 U))
l : Filter (𝓒 U) := 𝓝 f ⊓ 𝓟 (𝓙 U)
this : NeBot l
h1 : Tendsto id l (𝓝 f)
h2 : ∀ᶠ (a : 𝓒 U) in l, id a ∈ 𝓙 U
⊢ InjOn f U ∨ ∃ w, EqOn f (fun x => w) U