awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x : ℕ
H :
  ∀ j ≥ x,
    |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2 ∧
      |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯ -
                  CauSeq.const abs
                    (CauSeq.lim
                      (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯))) :
              ℕ → ℝ)
            j| <
        ε / 2
j : ℕ
ij : j ≥ x
H₁ :
  |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯ -
              CauSeq.const abs
                (CauSeq.lim
                  (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).re) ⋯))) :
          ℕ → ℝ)
        j| <
    ε / 2
H₂ :
  |(↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯ -
              CauSeq.const abs
                (CauSeq.lim
                  (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯))) :
          ℕ → ℝ)
        j| <
    ε / 2
⊢ |((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j).re| +
      |((↑(f - CauSeq.const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) j).im| <
    ε

Tactic:
simpa using add_lt_add H₁ H₂

Premises used: add_lt_add
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ CauSeq.IsComplete (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖

Tactic:
⟨fun f ↦ ⟨limAux f, equiv_limAux f⟩⟩

Premises used: Complex.limAux, Exists.intro, Complex.equiv_limAux, CauSeq.IsComplete.mk
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
this : IsAbsoluteValue (S := ℝ) fun (x : ℂ) ↦ ‖x‖ := ⋯
x : ℕ
⊢ ((↑(const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) x).re =
    ((↑(const (fun (x : ℂ) ↦ ‖x‖) ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I)) : ℕ → ℂ) x).re

Tactic:
simp [limAux, cauSeqRe, ofReal]

Premises used: Complex.ofReal, Complex.limAux, Complex.cauSeqRe
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
this : IsAbsoluteValue (S := ℝ) fun (x : ℂ) ↦ ‖x‖ := ⋯
x : ℕ
⊢ ((↑(const (fun (x : ℂ) ↦ ‖x‖) (limAux f)) : ℕ → ℂ) x).im =
    ((↑(const (fun (x : ℂ) ↦ ‖x‖) ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I)) : ℕ → ℂ) x).im

Tactic:
simp [limAux, cauSeqIm, ofReal]

Premises used: Complex.ofReal, Complex.cauSeqIm, Complex.limAux
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
rw : (cauSeqRe f).lim = ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I).re
⊢ (cauSeqRe f).lim = f.lim.re

Tactic:
rw [lim_eq_lim_im_add_lim_re]

Premises used: Complex.lim_eq_lim_im_add_lim_re
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ (cauSeqRe f).lim = ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I).re

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
rw : (cauSeqIm f).lim = ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I).im
⊢ (cauSeqIm f).lim = f.lim.im

Tactic:
rw [lim_eq_lim_im_add_lim_re]

Premises used: Complex.lim_eq_lim_im_add_lim_re
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ (cauSeqIm f).lim = ((↑(cauSeqRe f).lim : ℂ) + (↑(cauSeqIm f).lim : ℂ) * I).im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun (x : ℂ) ↦ ‖x‖) ((↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i) < ε
j : ℕ
hj : j ≥ i
simp_rw : ‖(↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i‖ < ε
⊢ (fun (x : ℂ) ↦ ‖x‖)
      (HSub.hSub (α := ℂ) ((fun (n : ℕ) ↦ ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑f : ℕ → ℂ) n) : ℂ)) j)
        ((fun (n : ℕ) ↦ ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑f : ℕ → ℂ) n) : ℂ)) i)) <
    ε

Tactic:
simp_rw [← map_sub, norm_conj]

Premises used: Complex.norm_conj, map_sub
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun (x : ℂ) ↦ ‖x‖) ((↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖(↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i‖ < ε

Tactic:
hi j hj
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun (x : ℂ) ↦ ‖x‖) ((↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖(↑f : ℕ → ℂ) j - (↑f : ℕ → ℂ) i‖ < ε

Tactic:
exact hi j hj
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ (cauSeqConj f).lim.re = re ((starRingEnd ℂ : (a : ℂ) → ℂ) f.lim)

Tactic:
simp [cauSeqConj, (lim_re _).symm, cauSeqRe]

Premises used: Eq.symm, Complex.cauSeqRe, Complex.cauSeqConj, Complex.lim_re
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
simp :
  CauSeq.lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ -((↑f : ℕ → ℂ) n).im) ⋯) =
    (-Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯).lim
⊢ (cauSeqConj f).lim.im = im ((starRingEnd ℂ : (a : ℂ) → ℂ) f.lim)

Tactic:
simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]

Premises used: Complex.cauSeqIm, Complex.lim_im, CauSeq.lim_neg, Eq.symm, Complex.cauSeqConj
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ CauSeq.lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ -((↑f : ℕ → ℂ) n).im) ⋯) =
    (-Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑f : ℕ → ℂ) n).im) ⋯).lim

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
f : CauSeq (α := ℝ) ℂ fun (x : ℂ) ↦ ‖x‖
⊢ (cauSeqNorm f).lim = ‖f.lim‖

Tactic:
lim_eq_of_equiv_const fun ε ε0 ↦
    let ⟨i, hi⟩ := equiv_lim f ε ε0
    ⟨i, fun j hj => lt_of_le_of_lt (abs_norm_sub_norm_le _ _) (hi j hj)⟩

Premises used: lt_of_le_of_lt, _private.0.Complex.lim_norm.match_1, Exists, CauSeq.equiv_lim, abs_norm_sub_norm_le, CauSeq.lim_eq_of_equiv_const, CauSeq.lim, Exists.intro, Subtype.val
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
s : ℂ
hs : 0 < s.re
⊢ s ≠ 0

Tactic:
fun h ↦ (zero_re ▸ h ▸ hs).false

Premises used: Not
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
s : ℂ
hs : 1 < s.re
⊢ s ≠ 0

Tactic:
ne_zero_of_re_pos <| zero_lt_one.trans hs

Premises used: zero_lt_one, LT.lt.trans, Complex.ne_zero_of_re_pos
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
s : ℂ
hs : 0 < s.re
⊢ (-s).re ≠ 0

Tactic:
ne_iff_lt_or_gt.mpr <| Or.inl <| neg_re s ▸ (neg_lt_zero.mpr hs)

Premises used: Iff.mpr, ne_iff_lt_or_gt, Or.inl
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
s : ℂ
hs : 1 < s.re
⊢ (-s).re ≠ 0

Tactic:
re_neg_ne_zero_of_re_pos <| zero_lt_one.trans hs

Premises used: zero_lt_one, Complex.re_neg_ne_zero_of_re_pos, LT.lt.trans
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 = 1

Tactic:
replace hz := sq_eq_one_iff.mpr (.inl hz)
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : HPow.hPow (β := ℕ) ‖z‖ 2 = 1
⊢ z.re * z.re + z.im * z.im = 1

Tactic:
rw [Complex.sq_norm, normSq_apply] at hz

Premises used: Complex.sq_norm, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.Norm
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
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
⊢ z.im * z.im = 1 - z.re * z.re

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : ‖z‖ = 1
⊢ 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
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : ‖z‖ = 1
this : z.im * z.im = 1 - z.re * z.re
simp : (z.re - 1) * (z.re - 1) + (1 - z.re * z.re) = 2 * (1 - z.re)
⊢ HPow.hPow (β := ℕ) ‖z - 1‖ 2 = 2 * (1 - z.re)

Tactic:
simp [Complex.sq_norm, normSq_apply, this]

Premises used: Complex.sq_norm, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : ‖z‖ = 1
this : z.im * z.im = 1 - z.re * z.re
⊢ (z.re - 1) * (z.re - 1) + (1 - z.re * z.re) = 2 * (1 - z.re)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.sphere 0 1) z
⊢ ‖z‖ = 1

Tactic:
simpa using hz
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
nlinarith : 1 - HPow.hPow (β := ℕ) x 2 < 0 → 1 - HPow.hPow (β := ℕ) x 2 - 0 + (0 - (-1 - x) * (x - 1)) = 0
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) x 2

Tactic:
nlinarith [abs_le.mp hx]

Premises used: abs_le, Iff.mp
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑x : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x 2) : ℂ)) : ℝ) (1 : ℝ)

Tactic:
simp [mul_comm I, normSq_add_mul_I,
    Real.sq_sqrt (x := 1 - x ^ 2) (by nlinarith [abs_le.mp hx])]

Premises used: Real.sq_sqrt, Complex.normSq_add_mul_I, mul_comm, Complex.I
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
rw : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (-(↑x : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x 2) : ℂ)) : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((↑x : ℂ) - I * (↑√(1 - HPow.hPow (β := ℕ) x 2) : ℂ)) : ℝ) (1 : ℝ)

Tactic:
rw [← normSq_neg, neg_sub', sub_neg_eq_add]

Premises used: neg_sub', Complex.normSq_neg, sub_neg_eq_add
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖-x‖ ≤ 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (-(↑x : ℂ) + I * (↑√(1 - HPow.hPow (β := ℕ) x 2) : ℂ)) : ℝ) (1 : ℝ)

Tactic:
simpa using normSq_ofReal_add_I_mul_sqrt_one_sub (x := -x) (by simpa)

Premises used: Complex.normSq_ofReal_add_I_mul_sqrt_one_sub
-- 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)
⊢ 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
-- 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)
⊢ 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)
-- 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)
⊢ AnalyticOnNhd ℂ f (ball z₀ r)

Tactic:
have h3 : AnalyticOnNhd ℂ f (ball z₀ r) := h.differentiableOn.analyticOnNhd isOpen_ball
-- 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)
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
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
linarith₇ linarith₈ : ‖f z - v‖ < ε / 2 → GT.gt (α := ℝ) 2 0
⊢ ε / 2 ≤ ‖f z - v‖

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₀)]

Premises used: mem_ball_iff_norm, norm_sub_sub_norm_sub_le_norm_sub, Iff.mp
-- 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)
⊢ ∀ 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₀)]
-- 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‖
⊢ ‖f z₀ - v‖ < ε / 2

Tactic:
simpa [← dist_eq_norm, dist_comm] using mem_ball.mp hv

Premises used: dist_eq_norm, dist_comm, Metric.mem_ball, Iff.mp
-- 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‖
⊢ ‖f z₀ - v‖ < ε / 2

Tactic:
have h5 : ‖f z₀ - v‖ < ε / 2 := by simpa [← dist_eq_norm, dist_comm] using mem_ball.mp hv
-- 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 ∈ ball z₀ r, IsLocalMin (β := ℝ) (fun (z : ℂ) ↦ ‖f z - v‖) z

Tactic:
exists_isLocalMin_mem_ball h2 (mem_closedBall_self hr.le) fun z hz => h5.trans_le (h4 z hz)

Premises used: Metric.exists_isLocalMin_mem_ball, LT.lt.le, LT.lt.trans_le, Metric.mem_closedBall_self
-- 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
obtain :
  ∀ (z : ℂ) (hz1 : z ∈ ball z₀ r) (hz2 : IsLocalMin (β := ℝ) (fun (z : ℂ) ↦ ‖f z - v‖) z), v ∈ f '' closedBall z₀ r
⊢ 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)

Premises used: Metric.exists_isLocalMin_mem_ball, LT.lt.le, Metric.ball, LT.lt.trans_le, Metric.mem_closedBall_self
-- 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
⊢ v ∈ f '' closedBall z₀ r

Tactic:
⟨z, ball_subset_closedBall hz1, sub_eq_zero.mp ?_⟩

Premises used: Metric.ball_subset_closedBall, Set.Mem, sub_eq_zero, setOf, And.intro, Exists.intro, Iff.mp, Set.image
-- 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
refine : f z - v = 0
⊢ v ∈ f '' closedBall z₀ r

Tactic:
refine ⟨z, ball_subset_closedBall hz1, sub_eq_zero.mp ?_⟩
-- 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
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ f z - v) y

Tactic:
have h6 := h1.differentiableOn.eventually_differentiableAt (isOpen_ball.mem_nhds hz1)
-- 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
⊢ f z - v = 0

Tactic:
(eventually_eq_or_eq_zero_of_isLocalMin_norm h6 hz2).resolve_left fun key => ?_

Premises used: Or.resolve_left, Complex.eventually_eq_or_eq_zero_of_isLocalMin_norm
-- 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
refine : ∀ (key : ∀ᶠ (z_1 : ℂ) in 𝓝 z, f z_1 - v = f z - v), False
⊢ f z - v = 0

Tactic:
refine (eventually_eq_or_eq_zero_of_isLocalMin_norm h6 hz2).resolve_left fun key => ?_

Premises used: Or.resolve_left, Complex.eventually_eq_or_eq_zero_of_isLocalMin_norm
-- 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
h₁ : ∀ (h : ℂ), f h - v = f z - v → f h = f z
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, f w = f z

Tactic:
filter_upwards [key] with h
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h_1 : 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
h : ℂ
⊢ f h - v = f z - v → f h = f z

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

Tactic:
have h7 : ∀ᶠ w in 𝓝 z, f w = f z := by filter_upwards [key] with h; simp
-- 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
⊢ ∃ᶠ (w : ℂ) in 𝓝[≠] z, f w = f z

Tactic:
replace h7 : ∃ᶠ w in 𝓝[≠] z, f w = f z := (h7.filter_mono nhdsWithin_le_nhds).frequently
-- 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
⊢ IsPreconnected (ball z₀ r)

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