awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
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 ℂ (F := ℂ) (fun (z : ℂ) ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (Y := ℝ) (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 ℂ (F := ℂ) (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)
⊢ EqOn f (fun (x : ℂ) ↦ f z) (ball z₀ r)

Tactic:
have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOnNhd_const h8 hz1 h7
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
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 ℂ (F := ℂ) (fun (z : ℂ) ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (Y := ℝ) (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 ℂ (F := ℂ) (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)
⊢ f z = f z₀

Tactic:
have h10 : f z = f z₀ := (h9 (mem_ball_self hr)).symm
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
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 ℂ (F := ℂ) (fun (z : ℂ) ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (Y := ℝ) (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 ℂ (F := ℂ) (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

Tactic:
not_eventually.mpr hz₀ (mem_of_superset (ball_mem_nhds z₀ hr) (h10 ▸ h9))

Premises used: Iff.mpr, Eq.rec, Metric.ball_mem_nhds, Filter.not_eventually, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
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 ℂ (F := ℂ) (fun (z : ℂ) ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (Y := ℝ) (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 ℂ (F := ℂ) (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

Tactic:
exact not_eventually.mpr hz₀ (mem_of_superset (ball_mem_nhds z₀ hr) (h10 ▸ h9))

Premises used: Iff.mpr, Eq.rec, Metric.ball_mem_nhds, Filter.not_eventually, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
⊢ (∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀) ∨ 𝓝 (f z₀) ≤ map f (𝓝 z₀)

Tactic:
or_iff_not_imp_left.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
refine : ∀ (h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀), 𝓝 (f z₀) ≤ map f (𝓝 z₀)
⊢ (∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀) ∨ 𝓝 (f z₀) ≤ map f (𝓝 z₀)

Tactic:
refine or_iff_not_imp_left.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
⊢ 𝓝 (f z₀) ≤ map f (𝓝 z₀)

Tactic:
(nhds_basis_ball.le_basis_iff (nhds_basis_closedBall.map f)).mpr fun R hR => ?_

Premises used: Iff.mpr, Filter.HasBasis.le_basis_iff, Filter.HasBasis.map, Metric.nhds_basis_ball, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
refine : ∀ (R : ℝ) (hR : 0 < R), ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
⊢ 𝓝 (f z₀) ≤ map f (𝓝 z₀)

Tactic:
refine (nhds_basis_ball.le_basis_iff (nhds_basis_closedBall.map f)).mpr fun R hR => ?_

Premises used: Iff.mpr, Filter.HasBasis.le_basis_iff, Filter.HasBasis.map, Metric.nhds_basis_ball, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀

Tactic:
have h1 := (hf.eventually_eq_or_eventually_ne analyticAt_const).resolve_left h
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z

Tactic:
have h2 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).eventually_mem hf
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
⊢ ∃ ρ > 0, AnalyticOnNhd ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀

Tactic:
simpa only [setOf_and, subset_inter_iff] using
      nhds_basis_closedBall.mem_iff.mp (h2.and (eventually_nhdsWithin_iff.mp h1))

Premises used: Set.setOf_and, Filter.HasBasis.mem_iff, Set.subset_inter_iff, Filter.Eventually.and, eventually_nhdsWithin_iff, Iff.mp, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
obtain :
  ∀ (ρ : ℝ) (hρ : ρ > 0) (h3 : AnalyticOnNhd ℂ f (closedBall z₀ ρ)) (h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀),
    ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R

Tactic:
obtain ⟨ρ, hρ, h3, h4⟩ :
    ∃ ρ > 0, AnalyticOnNhd ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ := by
    simpa only [setOf_and, subset_inter_iff] using
      nhds_basis_closedBall.mem_iff.mp (h2.and (eventually_nhdsWithin_iff.mp h1))
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h3 : AnalyticOnNhd ℂ f (closedBall z₀ ρ)
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
⊢ DiffContOnCl ℂ f (ball z₀ ρ)

Tactic:
replace h3 : DiffContOnCl ℂ f (ball z₀ ρ) :=
    ⟨h3.differentiableOn.mono ball_subset_closedBall,
      (closure_ball z₀ hρ.lt.ne.symm).symm ▸ h3.continuousOn⟩
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
⊢ 0 < r

Tactic:
have hr : 0 < r := lt_inf_iff.mpr ⟨hρ, hR⟩
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
⊢ closedBall z₀ r ⊆ closedBall z₀ ρ

Tactic:
have h5 : closedBall z₀ r ⊆ closedBall z₀ ρ := closedBall_subset_closedBall inf_le_left
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
⊢ DiffContOnCl ℂ f (ball z₀ r)

Tactic:
have h6 : DiffContOnCl ℂ f (ball z₀ r) := h3.mono (ball_subset_ball inf_le_left)
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
⊢ ∀ z ∈ sphere z₀ r, f z ≠ f z₀

Tactic:
have h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀ := fun z hz =>
    h4 z (h5 (sphere_subset_closedBall hz)) (ne_of_mem_sphere hz hr.ne.symm)
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
⊢ (sphere z₀ r).Nonempty

Tactic:
have h8 : (sphere z₀ r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)

Tactic:
have h9 : ContinuousOn (fun x => ‖f x - f z₀‖) (sphere z₀ r) := continuous_norm.comp_continuousOn
    ((h6.sub_const (f z₀)).continuousOn_ball.mono sphere_subset_closedBall)
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)
obtain :
  ∀ (x : ℂ) (hx : x ∈ sphere z₀ r) (hfx : IsMinOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r) x),
    ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R

Tactic:
obtain ⟨x, hx, hfx⟩ := (isCompact_sphere z₀ r).exists_isMinOn h8 h9

Premises used: isCompact_sphere, IsCompact.exists_isMinOn
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r) x
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R

Tactic:
⟨‖f x - f z₀‖ / 2, half_pos (norm_sub_pos_iff.mpr (h7 x hx)), ?_⟩

Premises used: Iff.mpr, Norm.norm, half_pos, HSub.hSub, HDiv.hDiv, And.intro, Exists.intro, OfNat.ofNat, norm_sub_pos_iff
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r) x
refine : ball (f z₀) (‖f x - f z₀‖ / 2) ⊆ f '' closedBall z₀ R
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R

Tactic:
refine ⟨‖f x - f z₀‖ / 2, half_pos (norm_sub_pos_iff.mpr (h7 x hx)), ?_⟩
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r) x
h₁ : r ≤ R
⊢ f '' closedBall z₀ r ⊆ f '' closedBall z₀ R

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r) x
⊢ r ≤ R

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r) x
⊢ r ≤ R

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ρ : ℝ
hρ : ρ > 0
h4 : ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀
h3 : DiffContOnCl ℂ f (ball z₀ ρ)
r : ℝ := min ρ R
hr : 0 < r
h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
h6 : DiffContOnCl ℂ f (ball z₀ r)
h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀
h8 : (sphere z₀ r).Nonempty
h9 : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r)
x : ℂ
hx : x ∈ sphere z₀ r
hfx : IsMinOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x - f z₀‖) (sphere z₀ r) x
⊢ ball (f z₀) (‖f x - f z₀‖ / 2) ⊆ f '' closedBall z₀ R

Tactic:
exact (h6.ball_subset_image_closedBall hr (fun z hz => hfx hz) (not_eventually.mp h)).trans
    (by gcongr; exact inf_le_right)

Premises used: HasSubset.Subset.trans, Filter.not_eventually, Iff.mp, DiffContOnCl.ball_subset_image_closedBall
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
obtain :
  ∀ (r : ℝ) (hr : r > 0) (hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}),
    (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
obtain ⟨r, hr, hgr⟩ := isOpen_iff.mp (isOpen_analyticAt ℂ g) z₀ hg

Premises used: Metric.isOpen_iff, isOpen_analyticAt, Iff.mp, Complex
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
⊢ ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → AnalyticOnNhd ℂ (gray z) (ball 0 r)

Tactic:
fun z hz t ht => AnalyticAt.comp ?_ ?_

Premises used: AnalyticOnNhd, AnalyticAt.comp
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
refine_1 :
  ∀ (z : E) (hz : Membership.mem (γ := Set E) (sphere 0 1) z) (t : ℂ) (ht : Membership.mem (γ := Set ℂ) (ball 0 r) t),
    AnalyticAt ℂ g (ray z t)
refine_2 :
  ∀ (z : E) (hz : Membership.mem (γ := Set E) (sphere 0 1) z) (t : ℂ) (ht : Membership.mem (γ := Set ℂ) (ball 0 r) t),
    AnalyticAt ℂ (ray z) t
⊢ ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → AnalyticOnNhd ℂ (gray z) (ball 0 r)

Tactic:
refine fun z hz t ht => AnalyticAt.comp ?_ ?_

Premises used: AnalyticAt.comp
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
z : E
hz : Membership.mem (γ := Set E) (sphere 0 1) z
t : ℂ
ht : Membership.mem (γ := Set ℂ) (ball 0 r) t
⊢ ray z t ∈ ball z₀ r

Tactic:
simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using ht

Premises used: norm_smul, mem_sphere_zero_iff_norm, Iff.mp
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
z : E
hz : Membership.mem (γ := Set E) (sphere 0 1) z
t : ℂ
ht : Membership.mem (γ := Set ℂ) (ball 0 r) t
⊢ AnalyticAt ℂ g (ray z t)

Tactic:
exact hgr (by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using ht)
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
z : E
hz : Membership.mem (γ := Set E) (sphere 0 1) z
t : ℂ
ht : Membership.mem (γ := Set ℂ) (ball 0 r) t
⊢ AnalyticAt ℂ (ray z) t

Tactic:
analyticAt_const.add
        ((ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℂ ℂ) z).analyticAt t)

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.analyticAt, ContinuousLinearMap.id, analyticAt_const, AnalyticAt.add, Complex
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
z : E
hz : Membership.mem (γ := Set E) (sphere 0 1) z
t : ℂ
ht : Membership.mem (γ := Set ℂ) (ball 0 r) t
⊢ AnalyticAt ℂ (ray z) t

Tactic:
exact analyticAt_const.add
        ((ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℂ ℂ) z).analyticAt t)

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.analyticAt, ContinuousLinearMap.id, analyticAt_const, AnalyticAt.add, Complex
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
⊢ ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → AnalyticOnNhd ℂ (gray z) (ball 0 r)

Tactic:
have h1 : ∀ z ∈ sphere (0 : E) 1, AnalyticOnNhd ℂ (gray z) (ball 0 r) := by
    refine fun z hz t ht => AnalyticAt.comp ?_ ?_
    · exact hgr (by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using ht)
    · exact analyticAt_const.add
        ((ContinuousLinearMap.smulRight (ContinuousLinearMap.id ℂ ℂ) z).analyticAt t)
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
h1 : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → AnalyticOnNhd ℂ (gray z) (ball 0 r)
pos :
  ∀ (h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0),
    (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
neg :
  ∀ (h : ¬∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0),
    (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
by_cases h : ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0

Premises used: nhds, OfNat.ofNat, Metric.sphere
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
h1 : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
pos : ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
left
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun (z : E) (t : ℂ) ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun (z : E) ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x : E | AnalyticAt ℂ g x}
h1 : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀

Tactic:
eventually_of_mem (ball_mem_nhds z₀ hr) fun z hz => ?_

Premises used: Filter.eventually_of_mem, Metric.ball_mem_nhds