awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ (cauSeqConj f).lim.im = im ((starRingEnd ℂ : (a : ℂ) → ℂ) f.lim)
have simp : CauSeq.lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ -((↑f : ℕ → ℂ) n).im) sorry) =
  (-Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) sorry).lim
Tactic: simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (hypothesis)
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ z.im * z.im = 1 - z.re * z.re
have hz₁ : HPow.hPow (β := ℕ) ‖z‖ 2 = 1
Tactic: replace hz := sq_eq_one_iff.mpr (.inl hz)
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (hypothesis)
Goal:
z : ℂ
hz : HPow.hPow (β := ℕ) ‖z‖ 2 = 1
⊢ z.im * z.im = 1 - z.re * z.re
have hz₁ : z.re * z.re + z.im * z.im = 1
Tactic: rw [Complex.sq_norm, normSq_apply] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : z.re * z.re + z.im * z.im = 1
⊢ z.im * z.im = 1 - z.re * z.re
have linarith : z.im * z.im < 1 - z.re * z.re → -(z.re * z.re + z.im * z.im - 1) + (z.im * z.im - (1 - z.re * z.re)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : z.re * z.re + z.im * z.im = 1
linarith : z.im * z.im < 1 - z.re * z.re → -(z.re * z.re + z.im * z.im - 1) + (z.im * z.im - (1 - z.re * z.re)) = 0
⊢ z.im * z.im = 1 - z.re * z.re
have linarith₁ : 1 - z.re * z.re < z.im * z.im → z.re * z.re + z.im * z.im - 1 + (1 - z.re * z.re - z.im * z.im) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (hypothesis)
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ HPow.hPow (β := ℕ) ‖z - 1‖ 2 = 2 * (1 - z.re)
have this : z.im * z.im = 1 - z.re * z.re
Tactic: have : z.im * z.im = 1 - z.re * z.re := by
    replace hz := sq_eq_one_iff.mpr (.inl hz)
    rw [Complex.sq_norm, normSq_apply] at hz
    linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
hz : ‖z‖ = 1
this : z.im * z.im = 1 - z.re * z.re
⊢ HPow.hPow (β := ℕ) ‖z - 1‖ 2 = 2 * (1 - z.re)
have simp : (z.re - 1) * (z.re - 1) + (1 - z.re * z.re) = 2 * (1 - z.re)
Tactic: simp [Complex.sq_norm, normSq_apply, this]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
have nlinarith : 1 - HPow.hPow (β := ℕ) x 2 < 0 → 1 - HPow.hPow (β := ℕ) x 2 - 0 + (0 - (-1 - x) * (x - 1)) = 0
Tactic: nlinarith [abs_le.mp hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑x : ℂ) - I * (↑√(1 - HPow.hPow (β := ℕ) x 2) : ℂ)) : ℝ) (1 : ℝ)
have rw : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (-(↑x : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x 2) : ℂ)) : ℝ) (1 : ℝ)
Tactic: rw [← normSq_neg, neg_sub', sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ v ∈ f '' closedBall z₀ r
have h1 : DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ f z - v) (ball z₀ r)
Tactic: have h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r) := h.sub_const v
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ v ∈ f '' closedBall z₀ r
have h2 : ContinuousOn (Y := ℝ) (fun (z : ℂ) ↦ ‖f z - v‖) (closedBall z₀ r)
Tactic: have h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r) :=
    continuous_norm.comp_continuousOn (closure_ball z₀ hr.ne.symm ▸ h1.continuousOn)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ v ∈ f '' closedBall z₀ r
have h3 : AnalyticOnNhd ℂ f (ball z₀ r)
Tactic: have h3 : AnalyticOnNhd ℂ f (ball z₀ r) := h.differentiableOn.analyticOnNhd isOpen_ball
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
z : ℂ
hz : z ∈ sphere z₀ r
⊢ ε / 2 ≤ ‖f z - v‖
have linarith : ‖f z - v‖ < ε / 2 → 2 / 2 = 1
Tactic: linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball_iff_norm.1 hv,
      norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
z : ℂ
hz : z ∈ sphere z₀ r
linarith : ‖f z - v‖ < ε / 2 → 2 / 2 = 1
⊢ ε / 2 ≤ ‖f z - v‖
have linarith₁ : ‖f z - v‖ < ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball_iff_norm.1 hv,
      norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
z : ℂ
hz : z ∈ sphere z₀ r
linarith : ‖f z - v‖ < ε / 2 → 2 / 2 = 1
linarith₁ : ‖f z - v‖ < ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ε / 2 ≤ ‖f z - v‖
have linarith₂ : ‖f z - v‖ < ε / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball_iff_norm.1 hv,
      norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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)
z : ℂ
hz : z ∈ sphere z₀ r
linarith : ‖f z - v‖ < ε / 2 → 2 / 2 = 1
linarith₁ : ‖f z - v‖ < ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ‖f z - v‖ < ε / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : ‖f z - v‖ < ε / 2 → 2 / 2 = 1
linarith₄ : ‖f z - v‖ < ε / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ‖f z - v‖ < ε / 2 → GT.gt (α := ℝ) 2 0
⊢ ε / 2 ≤ ‖f z - v‖
have linarith₆ : ‖f z - v‖ < ε / 2 →
  2 * ‖f z - v‖ - 1 * ε + 2 * (ε - ‖f z - f z₀‖) + (2 * ‖v - f z₀‖ - 1 * ε) +
      2 * (‖f z - f z₀‖ - ‖v - f z₀‖ - ‖f z - v‖) =
    0
Tactic: linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball_iff_norm.1 hv,
      norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ v ∈ f '' closedBall z₀ r
have h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
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_iff_norm.1 hv,
      norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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‖
⊢ v ∈ f '' closedBall z₀ r
have h5 : ‖f z₀ - v‖ < ε / 2
Tactic: have h5 : ‖f z₀ - v‖ < ε / 2 := by simpa [← dist_eq_norm, dist_comm] using mem_ball.mp hv
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ v ∈ f '' closedBall z₀ r
have obtain : ∀ (z : ℂ) (hz1 : z ∈ ball z₀ r) (hz2 : IsLocalMin (β := ℝ) (fun (z : ℂ) ↦ ‖f z - v‖) z), v ∈ f '' closedBall z₀ r
Tactic: obtain ⟨z, hz1, hz2⟩ : ∃ z ∈ ball z₀ r, IsLocalMin (fun z => ‖f z - v‖) z :=
    exists_isLocalMin_mem_ball h2 (mem_closedBall_self hr.le) fun z hz => h5.trans_le (h4 z hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ v ∈ f '' closedBall z₀ r
have refine : f z - v = 0
Tactic: refine ⟨z, ball_subset_closedBall hz1, sub_eq_zero.mp ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ f z - v = 0
have h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ f z - v) y
Tactic: have h6 := h1.differentiableOn.eventually_differentiableAt (isOpen_ball.mem_nhds hz1)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ f z - v = 0
have refine : ∀ (key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v), False
Tactic: refine (eventually_eq_or_eq_zero_of_isLocalMin_norm h6 hz2).resolve_left fun key => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, f w = f z
have h₁ : ∀ (h : ℂ), f h - v = f z - v → f h = f z
Tactic: filter_upwards [key] with h
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ False
have h7 : ∀ᶠ (w : ℂ) in 𝓝 z, f w = f z
Tactic: have h7 : ∀ᶠ w in 𝓝 z, f w = f z := by filter_upwards [key] with h; simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ False
have h7₁ : ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z
Tactic: replace h7 : ∃ᶠ w in 𝓝[≠] z, f w = f z := (h7.filter_mono nhdsWithin_le_nhds).frequently
Cleared hypotheses: h7
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ False
have h8 : IsPreconnected (ball z₀ r)
Tactic: have h8 : IsPreconnected (ball z₀ r) := (convex_ball z₀ r).isPreconnected
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ False
have h9 : EqOn f (fun (x : ℂ) ↦ f z) (ball z₀ r)
Tactic: have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOnNhd_const h8 hz1 h7
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ False
have h10 : f z = f z₀
Tactic: have h10 : f z = f z₀ := (h9 (mem_ball_self hr)).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
⊢ (∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀) ∨ 𝓝 (f z₀) ≤ map f (𝓝 z₀)
have refine : ∀ (h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀), 𝓝 (f z₀) ≤ map f (𝓝 z₀)
Tactic: refine or_iff_not_imp_left.mpr fun h => ?_
-- 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₀
⊢ 𝓝 (f z₀) ≤ map f (𝓝 z₀)
have refine : ∀ (R : ℝ) (hR : 0 < R), ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
Tactic: refine (nhds_basis_ball.le_basis_iff (nhds_basis_closedBall.map f)).mpr fun R hR => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
Goal:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h1 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, f z ≠ f z₀
Tactic: have h1 := (hf.eventually_eq_or_eventually_ne analyticAt_const).resolve_left h
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
Tactic: have h2 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).eventually_mem hf
-- 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
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have 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
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))
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h3₁ : 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⟩
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have hr : 0 < r
Tactic: have hr : 0 < r := lt_inf_iff.mpr ⟨hρ, hR⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h5 : closedBall z₀ r ⊆ closedBall z₀ ρ
Tactic: have h5 : closedBall z₀ r ⊆ closedBall z₀ ρ := closedBall_subset_closedBall inf_le_left
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀ ρ
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h6 : DiffContOnCl ℂ f (ball z₀ r)
Tactic: have h6 : DiffContOnCl ℂ f (ball z₀ r) := h3.mono (ball_subset_ball inf_le_left)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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)
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h7 : ∀ 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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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₀
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h8 : (sphere z₀ r).Nonempty
Tactic: have h8 : (sphere z₀ r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
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
⊢ ∃ (i : ℝ), 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
have h9 : 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)