intro i x hx
case intro.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
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K (closedBall 0 (M / δ))
case intro.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
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ (_root_.deriv ∘ F) i x ∈ closedBall 0 (M / δ)