field_simp [hMp.lt.ne.symm, mul_comm]
case h.e'_4
ι : 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
e3 : z ∈ closedBall z δ
e4 : ↑w ∈ closedBall z δ
this : ‖z - ↑w‖ < ε / M
⊢ ε = M * (ε / M)
no goals