-- Mathlib/Analysis/Complex/Schwarz.lean
theorem schwarz_aux {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₁

Proof state:
case h.refine_1
R₁ R₂ : ℝ
c 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

Tactic:
have hz' : z ≠ c := ne_of_mem_sphere hz hr₀.ne'

Result:
case h.refine_1
R₁ R₂ : ℝ
c 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

Proof state:
R₁ R₂ : ℝ
c 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₁

Tactic:
rw [mem_sphere.1 hz]

Result:
R₁ R₂ : ℝ
c 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₁

Proof state:
R₁ R₂ : ℝ
c 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)

Tactic:
refine DifferentiableOn.diffContOnCl ?_

Result:
R₁ R₂ : ℝ
c 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))

Proof state:
R₁ R₂ : ℝ
c 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)

Tactic:
exact ((differentiableOn_dslope <| ball_mem_nhds _ hR₁).mpr hd).mono
  (closedBall_subset_ball hr.2)

Result:
no goals

Proof state:
case h
R₁ R₂ : ℝ
c 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

Tactic:
refine norm_le_of_forall_mem_frontier_norm_le isBounded_ball hd ?_ ?_

Result:
case h.refine_1
R₁ R₂ : ℝ
c 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 ∈ frontier (ball c r), ‖dslope f c z‖ ≤ R₂ / r

case h.refine_2
R₁ R₂ : ℝ
c 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)

Proof state:
case h
R₁ R₂ : ℝ
c 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

Tactic:
have hr₀ : 0 < r := dist_nonneg.trans_lt hr.1

Result:
case h
R₁ R₂ : ℝ
c 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