-- Mathlib/Analysis/Complex/LocallyUniformLimit.lean
theorem norm_cderiv_lt (hr : 0 < r) (hfM : ∀ w ∈ sphere z r, ‖f w‖ < M)
    (hf : ContinuousOn f (sphere z r)) : ‖cderiv r f z‖ < M / r

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : IsMaxOn (fun w => ‖f w‖) (sphere z r) x
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
exact ⟨‖f x‖, hfM x hx, hx'⟩

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2

Result:
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : IsMaxOn (fun w => ‖f w‖) (sphere z r) x
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ‖cderiv r f z‖ < M / r

Tactic:
obtain ⟨L, hL1, hL2⟩ : ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L := by
  have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
  have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
  obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2
  exact ⟨‖f x‖, hfM x hx, hx'⟩

Result:
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
L : ℝ
hL1 : L < M
hL2 : ∀ w ∈ sphere z r, ‖f w‖ ≤ L
⊢ ‖cderiv r f z‖ < M / r

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
L : ℝ
hL1 : L < M
hL2 : ∀ w ∈ sphere z r, ‖f w‖ ≤ L
⊢ ‖cderiv r f z‖ < M / r

Tactic:
exact (norm_cderiv_le hr hL2).trans_lt ((div_lt_div_iff_of_pos_right hr).mpr hL1)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L