refine ⟨⟨by tauto, fun f g => Subtype.ext⟩, ?_⟩
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ ClosedEmbedding (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val)
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
l1 : ∀ K ∈ compacts U, EquicontinuousOn Subtype.val K
l2 : ∀ K ∈ compacts U, ∀ x ∈ K, ∃ L, IsCompact L ∧ ∀ (i : ↑(𝓑 U Q)), ↑i x ∈ L
⊢ IsClosed (range (⇑(UniformOnFun.ofFun (compacts U)) ∘ Subtype.val))