Theorem: SuperAt.superNear (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ ∃ t, SuperNear f d t
Tactic:
rcases s.fa0.exists_ball_analyticOn with ⟨r0, r0p, fa⟩
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
⊢ ∃ t, SuperNear f d t

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
⊢ ∃ t, SuperNear f d t
Tactic:
rcases Metric.continuousAt_iff.mp (s.ga_of_fa (fa 0 (mem_ball_self r0p))).continuousAt (1 / 4)
    (by norm_num) with
  ⟨r1, r1p, gs⟩
State after:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
⊢ ∃ t, SuperNear f d t

State before:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
⊢ ∃ t, SuperNear f d t
Tactic:
set r := min r0 (min r1 (1 / 2))
State after:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ ∃ t, SuperNear f d t

State before:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ ∃ t, SuperNear f d t
Tactic:
use ball 0 r
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ SuperNear f d (ball 0 r)

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ SuperNear f d (ball 0 r)
Tactic:
have rp : 0 < r := by bound
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
⊢ SuperNear f d (ball 0 r)

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
⊢ SuperNear f d (ball 0 r)
Tactic:
have r2 : r ≤ 1 / 2 := le_trans (min_le_right _ _) (min_le_right _ _)
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
⊢ SuperNear f d (ball 0 r)

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
⊢ SuperNear f d (ball 0 r)
Tactic:
have rr1 : r ≤ r1 := le_trans (min_le_right r0 _) (min_le_left r1 _)
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
⊢ SuperNear f d (ball 0 r)

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
⊢ SuperNear f d (ball 0 r)
Tactic:
simp only [g0, dist_zero_right, Complex.norm_eq_abs, Complex.dist_eq, sub_zero] at gs
State after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
gs : ∀ {x : ℂ}, Complex.abs x < r1 → Complex.abs (g f d x - 1) < 1 / 4
⊢ SuperNear f d (ball 0 r)

State before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
gs : ∀ {x : ℂ}, Complex.abs x < r1 → Complex.abs (g f d x - 1) < 1 / 4
⊢ SuperNear f d (ball 0 r)
Tactic:
exact s.super_on_ball rp r2 (fa.mono (Metric.ball_subset_ball (min_le_left r0 _))) (fun {z} zr ↦
  gs (lt_of_lt_of_le zr rr1))
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
⊢ 1 / 4 > 0
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ 0 < r
Tactic:
bound
State after:
no goals