awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have 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
Tactic: obtain ⟨x, hx, hfx⟩ := (isCompact_sphere z₀ r).exists_isMinOn h8 h9
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
have refine : ball (f z₀) (‖f x - f z₀‖ / 2) ⊆ f '' closedBall z₀ R
Tactic: refine ⟨‖f x - f z₀‖ / 2, half_pos (norm_sub_pos_iff.mpr (h7 x hx)), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ f '' closedBall z₀ r ⊆ f '' closedBall z₀ R
have h₁ : r ≤ R
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have 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₀)
Tactic: obtain ⟨r, hr, hgr⟩ := isOpen_iff.mp (isOpen_analyticAt ℂ g) z₀ hg
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
have 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)
Tactic: refine fun z hz t ht => AnalyticAt.comp ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
⊢ ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 1) z → AnalyticOnNhd ℂ (gray z) (ball 0 r)
have 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
Tactic: refine fun z hz t ht => AnalyticAt.comp ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have h1 : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have 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₀)
Tactic: by_cases h : ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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₀)
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have 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₀)
Tactic: by_cases h : ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have pos : ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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₀
have pos : ∀ (z : E) (hz : z ∈ ball z₀ r), g z = g z₀
Tactic: refine eventually_of_mem (ball_mem_nhds z₀ hr) fun z hz => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
have h' : z ≠ z₀
Tactic: refine (eq_or_ne z z₀).casesOn (congr_arg g) fun h' => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
⊢ g z = g z₀
have h'₁ : ‖z - z₀‖ ≠ 0
Tactic: replace h' : ‖z - z₀‖ ≠ 0 := by simpa only [Ne, norm_eq_zero, sub_eq_zero]
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
have e1 : IsPreconnected (α := ℂ) (ball 0 r)
Tactic: have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
have e2 : 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']
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
have h1₁ : AnalyticOnNhd ℂ (gray w) (ball 0 r)
Tactic: specialize h1 w e2
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
⊢ ∀ (t : ℂ), Membership.mem (γ := Set ℂ) (ball 0 r) t → gray w t = g z₀
have apply : gray w =ᶠ[𝓝 0] fun (x : ℂ) ↦ g z₀
Tactic: apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀)
⊢ g z = g z₀
have h3 : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
⊢ g z = g z₀
have h4 : ‖z - z₀‖ < r
Tactic: have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using mem_ball.mp hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ g z = g z₀
have h4₁ : Membership.mem (γ := Set ℂ) (ball 0 r) (↑‖z - z₀‖ : ℂ)
Tactic: replace h4 : ↑‖z - z₀‖ ∈ ball (0 : ℂ) r := by simpa
Cleared hypotheses: h4
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have neg : 𝓝 (g z₀) ≤ map g (𝓝 z₀)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have 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₀)
Tactic: obtain ⟨z, hz, hrz⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have h1₁ : AnalyticAt ℂ (gray z) 0
Tactic: specialize h1 z hz 0 (mem_ball_self hr)
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
have h7 : 𝓝 (gray z 0) ≤ map (gray z) (𝓝 0)
Tactic: have h7 := h1.eventually_constant_or_nhds_le_map_nhds_aux.resolve_left hrz
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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 (𝓝 z₀)
have h7₁ : 𝓝 (g z₀) ≤ (map g ∘ map (ray z)) (𝓝 0)
Tactic: rw [show gray z 0 = g z₀ by simp [gray, ray], ← map_compose] at h7
Cleared hypotheses: h7
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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₀)
have neg : map (ray z) (𝓝 0) ≤ 𝓝 z₀
Tactic: refine h7.trans (map_mono ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ map (ray z) (𝓝 0) ≤ 𝓝 z₀
have h10 : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (t : ℂ) ↦ z₀ + t • z
Tactic: have h10 : Continuous fun t : ℂ => z₀ + t • z := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
have 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)
Tactic: by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
have 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)
Tactic: by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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₀
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
have 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)
Tactic: obtain ⟨z₀, hz₀, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
have h₁ : ∀ x ∈ U, ¬∀ᶠ (z : E) in 𝓝 x, g z = g x
Tactic: simp only [not_exists, not_and] at h
Cleared hypotheses: h