obtain ⟨Q, hQ1, hQ2⟩ := h1 _ e1
case intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q
case intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q