have e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M := by simpa [MapsTo] using hM i
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
⊢ dist (F i z) (F i ↑w) < ε
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
e2 : ∀ x ∈ closedBall z δ, ‖_root_.deriv (F i) x‖ ≤ M
⊢ dist (F i z) (F i ↑w) < ε