awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (hz : z ∈ ball z₀ r), g z = g z₀
⊢ ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀

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

Premises used: Filter.eventually_of_mem, Metric.ball_mem_nhds
-- 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
hz : z ∈ ball z₀ r
⊢ g z = g z₀

Tactic:
(eq_or_ne z z₀).casesOn (congr_arg g) fun h' => ?_

Premises used: Or.casesOn, eq_or_ne
-- 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
hz : z ∈ ball z₀ r
⊢ z ≠ z₀

Tactic:
refine (eq_or_ne z z₀).casesOn (congr_arg g) fun h' => ?_
-- 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
hz : z ∈ ball z₀ r
h' : z ≠ z₀
⊢ ‖z - z₀‖ ≠ 0

Tactic:
simpa only [Ne, norm_eq_zero, sub_eq_zero]

Premises used: norm_eq_zero, sub_eq_zero, Ne
-- 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
hz : z ∈ ball z₀ r
h' : z ≠ z₀
⊢ ‖z - z₀‖ ≠ 0

Tactic:
replace h' : ‖z - z₀‖ ≠ 0 := by simpa only [Ne, norm_eq_zero, sub_eq_zero]
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
⊢ IsPreconnected (α := ℂ) (ball 0 r)

Tactic:
have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
e1 : IsPreconnected (α := ℂ) (ball 0 r)
⊢ Membership.mem (γ := Set E) (sphere 0 1) w

Tactic:
simp [w, norm_smul, inv_mul_cancel₀ h']

Premises used: norm_smul, inv_mul_cancel₀
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
e1 : IsPreconnected (α := ℂ) (ball 0 r)
⊢ Membership.mem (γ := Set E) (sphere 0 1) w

Tactic:
have e2 : w ∈ sphere (0 : E) 1 := by simp [w, norm_smul, inv_mul_cancel₀ h']
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
e1 : IsPreconnected (α := ℂ) (ball 0 r)
e2 : Membership.mem (γ := Set E) (sphere 0 1) w
⊢ AnalyticOnNhd ℂ (gray w) (ball 0 r)

Tactic:
specialize h1 w e2
-- 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}
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
e1 : IsPreconnected (α := ℂ) (ball 0 r)
e2 : Membership.mem (γ := Set E) (sphere 0 1) w
h1 : AnalyticOnNhd ℂ (gray w) (ball 0 r)
apply : gray w =ᶠ[𝓝 0] fun (x : ℂ) ↦ g z₀
⊢ ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀

Tactic:
apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr)

Premises used: Metric.mem_ball_self, analyticOnNhd_const, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
-- 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}
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
e1 : IsPreconnected (α := ℂ) (ball 0 r)
e2 : Membership.mem (γ := Set E) (sphere 0 1) w
h1 : AnalyticOnNhd ℂ (gray w) (ball 0 r)
⊢ gray w =ᶠ[𝓝 0] fun (x : ℂ) ↦ g z₀

Tactic:
simpa [ray, gray] using h w e2
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
⊢ ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀

Tactic:
have h3 : ∀ t ∈ ball (0 : ℂ) r, gray w t = g z₀ := by
      have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected
      have e2 : w ∈ sphere (0 : E) 1 := by simp [w, norm_smul, inv_mul_cancel₀ h']
      specialize h1 w e2
      apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr)
      simpa [ray, gray] using h w e2
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
⊢ ‖z - z₀‖ < r

Tactic:
simpa [dist_eq_norm] using mem_ball.mp hz

Premises used: dist_eq_norm, Metric.mem_ball, 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}
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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
⊢ ‖z - z₀‖ < r

Tactic:
have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using mem_ball.mp hz
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
h4 : ‖z - z₀‖ < r
⊢ Membership.mem (γ := Set ℂ) (ball 0 r) (↑‖z - z₀‖ : ℂ)

Tactic:
simpa
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
h4 : ‖z - z₀‖ < r
⊢ Membership.mem (γ := Set ℂ) (ball 0 r) (↑‖z - z₀‖ : ℂ)

Tactic:
replace h4 : ↑‖z - z₀‖ ∈ ball (0 : ℂ) r := by simpa
-- 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
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
h4 : Membership.mem (γ := Set ℂ) (ball 0 r) (↑‖z - z₀‖ : ℂ)
⊢ g z = g z₀

Tactic:
simpa only [ray, gray, w, smul_smul, mul_inv_cancel₀ h', one_smul, add_sub_cancel,
      Function.comp_apply, coe_smul] using h3 (↑‖z - z₀‖) h4

Premises used: Norm.norm, mul_inv_cancel₀, HSub.hSub, smul_smul, Complex.ofReal, one_smul, add_sub_cancel, Complex.coe_smul, Function.comp_apply
-- 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
neg : 𝓝 (g z₀) ≤ map g (𝓝 z₀)
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
right
-- 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
⊢ ∃ (x : E) (_ : Membership.mem (γ := Set E) (sphere 0 1) x), ¬∀ᶠ (t : ℂ) in 𝓝 0, gray x t = gray x 0

Tactic:
simp only [not_forall] at h

Premises used: Classical.not_forall
-- 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 : ∃ (x : E) (_ : Membership.mem (γ := Set E) (sphere 0 1) x), ¬∀ᶠ (t : ℂ) in 𝓝 0, gray x t = gray x 0
neg :
  ∀ (z : E) (hz : Membership.mem (γ := Set E) (sphere 0 1) z) (hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0),
    𝓝 (g z₀) ≤ map g (𝓝 z₀)
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
obtain ⟨z, hz, hrz⟩ := h
-- 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)
z : E
hz : Membership.mem (γ := Set E) (sphere 0 1) z
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ AnalyticAt ℂ (gray z) 0

Tactic:
specialize h1 z hz 0 (mem_ball_self hr)

Premises used: Metric.mem_ball_self, OfNat.ofNat
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
⊢ 𝓝 (gray z 0) ≤ map (gray z) (𝓝 0)

Tactic:
have h7 := h1.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hrz
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
h7 : 𝓝 (gray z 0) ≤ map (gray z) (𝓝 0)
⊢ gray z 0 = g z₀

Tactic:
simp [gray, ray]
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
h7 : 𝓝 (gray z 0) ≤ map (gray z) (𝓝 0)
⊢ 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)

Tactic:
rw [show gray z 0 = g z₀ by simp [gray, ray], ← map_compose] at h7

Premises used: Filter.map_compose
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
h7.trans (map_mono ?_)

Premises used: Filter.map_mono, LE.le.trans
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
neg : map (ray z) (𝓝 0) ≤ 𝓝 z₀
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
refine h7.trans (map_mono ?_)

Premises used: Filter.map_mono, LE.le.trans
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (t : ℂ) ↦ z₀ + t • z

Tactic:
fun_prop
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (t : ℂ) ↦ z₀ + t • z

Tactic:
have h10 : Continuous fun t : ℂ => z₀ + t • z := by fun_prop
-- 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
hrz : ¬∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
h1 : AnalyticAt ℂ (gray z) 0
h7 : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
h10 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (t : ℂ) ↦ z₀ + t • z
⊢ map (ray z) (𝓝 0) ≤ 𝓝 z₀

Tactic:
simpa using h10.tendsto 0

Premises used: Continuous.tendsto, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
pos :
  ∀ (h : ∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀),
    (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
      ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
neg :
  ∀ (h : ¬∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀),
    (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
      ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
pos :
  ∀ (z₀ : E) (hz₀ : z₀ ∈ U) (h : ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀),
    (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
      ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
obtain ⟨z₀, hz₀, h⟩ := h
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
z₀ : E
hz₀ : z₀ ∈ U
h : ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const hU hz₀ h⟩

Premises used: analyticOnNhd_const, Exists.intro, Or.inl, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
z₀ : E
hz₀ : z₀ ∈ U
h : ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const hU hz₀ h⟩

Premises used: Or.inl
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ¬∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ ∀ x ∈ U, ¬∀ᶠ (z : E) in 𝓝 x, g z = g x

Tactic:
simp only [not_exists, not_and] at h

Premises used: not_exists, not_and
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∀ x ∈ U, ¬∀ᶠ (z : E) in 𝓝 x, g z = g x
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
Or.inr fun s hs1 hs2 => isOpen_iff_mem_nhds.mpr ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds, Or.inr