E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
suffices ∀ᶠ r in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r by
  refine' ge_of_tendsto _ this
  exact (tendsto_const_nhds.div tendsto_id hR₁.ne').mono_left nhdsWithin_le_nhds
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
⊢ ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
rw [mem_ball] at hz
case h
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
⊢ ‖dslope f c z‖ ≤ R₂ / r
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
⊢ ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
filter_upwards [Ioo_mem_nhdsWithin_Iio ⟨hz, le_rfl⟩] with r hr
case h
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ ‖dslope f c z‖ ≤ R₂ / r
case h
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
⊢ ‖dslope f c z‖ ≤ R₂ / r
have hr₀ : 0 < r := dist_nonneg.trans_lt hr.1
case hd
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DiffContOnCl ℂ (dslope f c) (ball c r)

case h
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ‖dslope f c z‖ ≤ R₂ / r
case h
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ ‖dslope f c z‖ ≤ R₂ / r
replace hd : DiffContOnCl ℂ (dslope f c) (ball c r)
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ∀ (z : ℂ), z ∈ frontier (ball c r) → ‖dslope f c z‖ ≤ R₂ / r

case h.refine'_2
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ z ∈ closure (ball c r)
case h
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ‖dslope f c z‖ ≤ R₂ / r
refine' norm_le_of_forall_mem_frontier_norm_le bounded_ball hd _ _
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this : ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ Tendsto (fun c => R₂ / c) (𝓝[Iio R₁] R₁) (𝓝 (R₂ / R₁))
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this : ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
refine' ge_of_tendsto _ this
no goals
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this : ∀ᶠ (r : ℝ) in 𝓝[Iio R₁] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ Tendsto (fun c => R₂ / c) (𝓝[Iio R₁] R₁) (𝓝 (R₂ / R₁))
exact (tendsto_const_nhds.div tendsto_id hR₁.ne').mono_left nhdsWithin_le_nhds
case hd
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DifferentiableOn ℂ (dslope f c) (closure (ball c r))
case hd
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DiffContOnCl ℂ (dslope f c) (ball c r)
refine' DifferentiableOn.diffContOnCl _
case hd
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DifferentiableOn ℂ (dslope f c) (closedBall c r)
case hd
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DifferentiableOn ℂ (dslope f c) (closure (ball c r))
rw [closure_ball c hr₀.ne']
no goals
case hd
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
⊢ DifferentiableOn ℂ (dslope f c) (closedBall c r)
exact ((differentiableOn_dslope <| ball_mem_nhds _ hR₁).mpr hd).mono
  (closedBall_subset_ball hr.2)
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ∀ (z : ℂ), z ∈ sphere c r → ‖dslope f c z‖ ≤ R₂ / r
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ∀ (z : ℂ), z ∈ frontier (ball c r) → ‖dslope f c z‖ ≤ R₂ / r
rw [frontier_ball c hr₀.ne']
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
⊢ ‖dslope f c z‖ ≤ R₂ / r
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ ∀ (z : ℂ), z ∈ sphere c r → ‖dslope f c z‖ ≤ R₂ / r
intro z hz
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / r
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
⊢ ‖dslope f c z‖ ≤ R₂ / r
have hz' : z ≠ c := ne_of_mem_sphere hz hr₀.ne'
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ dist (f z) (f c) ≤ R₂
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / r
rw [dslope_of_ne _ hz', slope_def_module, norm_smul, norm_inv, mem_sphere_iff_norm.1 hz, ←
  div_eq_inv_mul, div_le_div_right hr₀, ← dist_eq_norm]
no goals
case h.refine'_1
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ dist (f z) (f c) ≤ R₂
exact le_of_lt (h_maps (mem_ball.2 (by rw [mem_sphere.1 hz]; exact hr.2)))
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ r < R₁
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ dist z c < R₁
rw [mem_sphere.1 hz]
no goals
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z✝ z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz✝ : dist z✝ c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z✝ c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
z : ℂ
hz : z ∈ sphere c r
hz' : z ≠ c
⊢ r < R₁
exact hr.2
case h.refine'_2
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ dist z c ≤ r
case h.refine'_2
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ z ∈ closure (ball c r)
rw [closure_ball c hr₀.ne', mem_closedBall]
no goals
case h.refine'_2
E : Type ?u.115
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R R₁ R₂ : ℝ
f✝ : ℂ → E
c z z₀ : ℂ
f : ℂ → ℂ
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : dist z c < R₁
hR₁ : 0 < R₁
r : ℝ
hr : r ∈ Ioo (dist z c) R₁
hr₀ : 0 < r
hd : DiffContOnCl ℂ (dslope f c) (ball c r)
⊢ dist z c ≤ r
exact hr.1.le