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

Tactic:
have h10 : f z = f z₀ := (h9 (mem_ball_self hr)).symm

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)
h10 : f z = f z₀
⊢ False

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
⊢ False

Tactic:
have h8 : IsPreconnected (ball z₀ r) := (convex_ball z₀ r).isPreconnected

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)
⊢ False

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
⊢ False

Tactic:
replace h7 : ∃ᶠ w in 𝓝[≠] z, f w = f z := (h7.filter_mono nhdsWithin_le_nhds).frequently

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
⊢ 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)
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)
⊢ v ∈ f '' closedBall z₀ r

Tactic:
have h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖ := fun z hz => by
  linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball.mp hv,
    norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]

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)
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‖
⊢ v ∈ f '' closedBall z₀ r

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‖
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
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, f w = f z

Tactic:
filter_upwards [key] with h

Result:
case h
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
h : ℂ
⊢ f h - v = f z - v → f h = f z

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)
z : ℂ
hz : z ∈ sphere z₀ r
⊢ ε / 2 ≤ ‖f z - v‖

Tactic:
linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball.mp hv,
  norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]

Result:
no goals