-- 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 ∈ frontier (ball c r), ‖dslope f c z‖ ≤ R₂ / r

Tactic:
rw [frontier_ball c 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 ∈ sphere c r, ‖dslope f c z‖ ≤ 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 : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩

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

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 ∈ sphere c r, ‖dslope f c z‖ ≤ R₂ / r

Tactic:
intro z hz

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
⊢ ‖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
hz' : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / r

Tactic:
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_iff_of_pos_right hr₀, ← dist_eq_norm]

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
⊢ dist (f z) (f 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) (closure (ball c r))

Tactic:
rw [closure_ball c hr₀.ne']

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) (closedBall 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₁
hr₀ : 0 < r
⊢ ‖dslope f c z‖ ≤ R₂ / r

Tactic:
replace hd : DiffContOnCl ℂ (dslope f c) (ball c r) := by
  refine DifferentiableOn.diffContOnCl ?_
  rw [closure_ball c hr₀.ne']
  exact ((differentiableOn_dslope <| ball_mem_nhds _ hR₁).mpr hd).mono
    (closedBall_subset_ball hr.2)

Result:
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

Proof state:
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)
⊢ dist z c ≤ r

Tactic:
exact hr.1.le

Result:
no goals

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 : z ∈ ball c R₁
hR₁ : 0 < R₁
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ Tendsto (HDiv.hDiv R₂) (𝓝[<] R₁) (𝓝 (R₂ / R₁))

Tactic:
exact (tendsto_const_nhds.div tendsto_id hR₁.ne').mono_left nhdsWithin_le_nhds

Result:
no goals

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
hz' : z ≠ c
⊢ dist (f z) (f c) ≤ R₂

Tactic:
exact le_of_lt (h_maps (mem_ball.2 (by rw [mem_sphere.1 hz]; exact hr.2)))

Result:
no goals

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 : ℝ) in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r

Tactic:
filter_upwards [Ioo_mem_nhdsLT hz] with r hr

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₁
⊢ ‖dslope f c z‖ ≤ R₂ / r

Proof state:
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)

Tactic:
rw [closure_ball c hr₀.ne', mem_closedBall]

Result:
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)
⊢ dist z c ≤ 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
⊢ r < R₁

Tactic:
exact hr.2

Result:
no goals

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 : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
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

Result:
R₁ R₂ : ℝ
c 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 𝓝[<] R₁, ‖dslope f c z‖ ≤ 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 : z ∈ ball c R₁
hR₁ : 0 < R₁
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
refine ge_of_tendsto ?_ this

Result:
R₁ R₂ : ℝ
c 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 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r
⊢ Tendsto (HDiv.hDiv R₂) (𝓝[<] R₁) (𝓝 (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 : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r

Tactic:
rw [mem_ball] at hz

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 : ℝ) in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r