exact ((hQ2 i).mono_right hM).mono_right <| closedBall_subset_closedBall le_sup_left
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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) (closedBall z δ) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
⊢ MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 (M ⊔ 1))
no goals