-- Mathlib/Analysis/Complex/OpenMapping.lean
theorem DiffContOnCl.ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball z₀ r)) (hr : 0 < r)
    (hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖) (hz₀ : ∃ᶠ z in 𝓝 z₀, f z ≠ f z₀) :
    ball (f z₀) (ε / 2) ⊆ f '' closedBall z₀ r

Proof state:
case intro.intro
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z => ‖f z - v‖) z
⊢ v ∈ f '' closedBall z₀ r

Tactic:
refine ⟨z, ball_subset_closedBall hz1, sub_eq_zero.mp ?_⟩

Result:
case intro.intro
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z => ‖f z - v‖) z
⊢ f z - v = 0

Proof state:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
⊢ ‖f z₀ - v‖ < ε / 2

Tactic:
simpa [← dist_eq_norm, dist_comm] using mem_ball.mp hv

Result:
no goals

Proof state:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
⊢ ball (f z₀) (ε / 2) ⊆ f '' closedBall z₀ r

Tactic:
rintro v hv

Result:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
⊢ v ∈ f '' closedBall z₀ r

Proof state:
case intro.intro
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z => ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z
h8 : IsPreconnected (ball z₀ r)
⊢ False

Tactic:
have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOnNhd_const h8 hz1 h7

Result:
case intro.intro
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z => ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
h7 : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z
h8 : IsPreconnected (ball z₀ r)
h9 : EqOn f (fun x => f z) (ball z₀ r)
⊢ False

Proof state:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
⊢ v ∈ f '' closedBall z₀ r

Tactic:
have h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r) := h.sub_const v

Result:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
⊢ v ∈ f '' closedBall z₀ r

Proof state:
case intro.intro
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z => ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y
⊢ f z - v = 0

Tactic:
refine (eventually_eq_or_eq_zero_of_isLocalMin_norm h6 hz2).resolve_left fun key => ?_

Result:
case intro.intro
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z => ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z => f z - v) y
key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v
⊢ False