have : ∃ M > 0, ∀ i, MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M) := by
  obtain ⟨Q, hQ1, hQ2⟩ := h1.deriv hU h2 (closedBall z δ) ⟨h, isCompact_closedBall _ _⟩
  obtain ⟨M, hM⟩ := hQ1.isBounded.subset_closedBall 0
  refine ⟨M ⊔ 1, by simp, fun i => ?_⟩
  exact ((hQ2 i).mono_right hM).mono_right <| closedBall_subset_closedBall le_sup_left
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
this : ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }