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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa : AnalyticAt ℂ f c
⊢ AnalyticAt ℂ (g f d) c
Tactic:
rcases fa.exists_ball_analyticOn with ⟨r, rp, fa⟩
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
⊢ AnalyticAt ℂ (g f d) c

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Tactic:
have o : IsOpen (ball c r) := isOpen_ball
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
⊢ AnalyticAt ℂ (g f d) c

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Tactic:
generalize ht : ball c r = t
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
t : Set ℂ
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
t : Set ℂ
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c
Tactic:
rw [ht] at fa o
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c
Tactic:
suffices h : AnalyticOn ℂ (g f d) t by rw [← ht] at h; exact h _ (mem_ball_self rp)
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticOn ℂ (g f d) t

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticOn ℂ (g f d) t
Tactic:
have ga : DifferentiableOn ℂ (g f d) (t \ {0}) := by
  have e : ∀ z : ℂ, z ∈ t \ {0} → g f d z = f z / z ^ d := by
    intro z zs; simp only [Set.mem_diff, Set.mem_singleton_iff] at zs
    simp only [g, zs.2, if_false]
  rw [differentiableOn_congr e]
  apply DifferentiableOn.div (fa.mono (Set.diff_subset _ _)).differentiableOn
  exact (Differentiable.pow differentiable_id _).differentiableOn
  intro z zs; exact pow_ne_zero _ (Set.mem_diff_singleton.mp zs).2
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ AnalyticOn ℂ (g f d) t

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ AnalyticOn ℂ (g f d) t
Tactic:
rw [analyticOn_iff_differentiableOn o]
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ DifferentiableOn ℂ (g f d) t

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
by_cases t0 : (0 : ℂ) ∉ t
State after:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t

case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : ¬0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t

State before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : ¬0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
simp only [Set.not_not_mem] at t0
State after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ DifferentiableOn ℂ (g f d) t

State before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
gc : ContinuousAt (g f d) 0
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
exact (Complex.differentiableOn_compl_singleton_and_continuousAt_iff (o.mem_nhds t0)).mp ⟨ga, gc⟩
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
h : AnalyticOn ℂ (g f d) t
⊢ AnalyticAt ℂ (g f d) c
Tactic:
rw [← ht] at h
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
h : AnalyticOn ℂ (g f d) (ball c r)
⊢ AnalyticAt ℂ (g f d) c

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
h : AnalyticOn ℂ (g f d) (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Tactic:
exact h _ (mem_ball_self rp)
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ DifferentiableOn ℂ (g f d) (t \ {0})
Tactic:
have e : ∀ z : ℂ, z ∈ t \ {0} → g f d z = f z / z ^ d := by
  intro z zs; simp only [Set.mem_diff, Set.mem_singleton_iff] at zs
  simp only [g, zs.2, if_false]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (g f d) (t \ {0})

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (g f d) (t \ {0})
Tactic:
rw [differentiableOn_congr e]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => f x / x ^ d) (t \ {0})

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => f x / x ^ d) (t \ {0})
Tactic:
apply DifferentiableOn.div (fa.mono (Set.diff_subset _ _)).differentiableOn
State after:
case hd
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => x ^ d) (t \ {0})

case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0

State before:
case hd
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ DifferentiableOn ℂ (fun x => x ^ d) (t \ {0})

case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0
Tactic:
exact (Differentiable.pow differentiable_id _).differentiableOn
State after:
case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0

State before:
case hx
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
⊢ ∀ x ∈ t \ {0}, x ^ d ≠ 0
Tactic:
intro z zs
State after:
case hx
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
z : ℂ
zs : z ∈ t \ {0}
⊢ z ^ d ≠ 0

State before:
case hx
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
e : ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
z : ℂ
zs : z ∈ t \ {0}
⊢ z ^ d ≠ 0
Tactic:
exact pow_ne_zero _ (Set.mem_diff_singleton.mp zs).2
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ ∀ z ∈ t \ {0}, g f d z = f z / z ^ d
Tactic:
intro z zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t \ {0}
⊢ g f d z = f z / z ^ d

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t \ {0}
⊢ g f d z = f z / z ^ d
Tactic:
simp only [Set.mem_diff, Set.mem_singleton_iff] at zs
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t ∧ ¬z = 0
⊢ g f d z = f z / z ^ d

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
z : ℂ
zs : z ∈ t ∧ ¬z = 0
⊢ g f d z = f z / z ^ d
Tactic:
simp only [g, zs.2, if_false]
State after:
no goals

State before:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
rw [Set.diff_singleton_eq_self t0] at ga
State after:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) t
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t

State before:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) t
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
exact ga
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ ContinuousAt (g f d) 0
Tactic:
rw [Metric.continuousAt_iff]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < ε

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < ε
Tactic:
intro e ep
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
e : ℝ
ep : e > 0
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
e : ℝ
ep : e > 0
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e
Tactic:
rcases Metric.eventually_nhds_iff.mp
    (Asymptotics.isBigOWith_iff.mp (s.approx.forall_isBigOWith (by linarith : e / 2 > 0))) with
  ⟨t, tp, h⟩
State after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e

State before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∃ δ > 0, ∀ {x : ℂ}, dist x 0 < δ → dist (g f d x) (g f d 0) < e
Tactic:
use t, tp
State after:
case right
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∀ {x : ℂ}, dist x 0 < t → dist (g f d x) (g f d 0) < e

State before:
case right
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
⊢ ∀ {x : ℂ}, dist x 0 < t → dist (g f d x) (g f d 0) < e
Tactic:
intro z zs
State after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
z : ℂ
zs : dist z 0 < t
⊢ dist (g f d z) (g f d 0) < e

State before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
h : ∀ ⦃y : ℂ⦄, dist y 0 < t → ‖f y - y ^ d‖ ≤ e / 2 * ‖y ^ d‖
z : ℂ
zs : dist z 0 < t
⊢ dist (g f d z) (g f d 0) < e
Tactic:
specialize h zs
State after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : ‖f z - z ^ d‖ ≤ e / 2 * ‖z ^ d‖
⊢ dist (g f d z) (g f d 0) < e

State before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : ‖f z - z ^ d‖ ≤ e / 2 * ‖z ^ d‖
⊢ dist (g f d z) (g f d 0) < e
Tactic:
simp only [Complex.norm_eq_abs] at h
State after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ dist (g f d z) (g f d 0) < e

State before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ dist (g f d z) (g f d 0) < e
Tactic:
simp only [g, Complex.dist_eq]
State after:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e

State before:
case right
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Tactic:
by_cases z0 : z = 0
State after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e

State before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Tactic:
simp only [z0, if_false, eq_self_iff_true, if_true]
State after:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1) < e

State before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1) < e
Tactic:
calc
  abs (f z / z ^ d - 1) = abs (f z * (z ^ d)⁻¹ - 1) := by rw [div_eq_mul_inv]
  _ = abs ((f z - z ^ d) * (z ^ d)⁻¹) := by
    rw [mul_sub_right_distrib, mul_inv_cancel (pow_ne_zero d z0)]
  _ = abs (f z - z ^ d) * (abs (z ^ d))⁻¹ := by rw [Complex.abs.map_mul, map_inv₀]
  _ ≤ e / 2 * abs (z ^ d) * (abs (z ^ d))⁻¹ := by bound
  _ = e / 2 * (abs (z ^ d) * (abs (z ^ d))⁻¹) := by ring
  _ ≤ e / 2 * 1 := by bound
  _ = e / 2 := by ring
  _ < e := half_lt_self ep
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
e : ℝ
ep : e > 0
⊢ e / 2 > 0
Tactic:
linarith
State after:
no goals

State before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ Complex.abs ((if z = 0 then 1 else f z / z ^ d) - if True then 1 else f 0 / 0 ^ d) < e
Tactic:
simp only [z0, sub_self, AbsoluteValue.map_zero]
State after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ 0 < e

State before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : z = 0
⊢ 0 < e
Tactic:
exact ep
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1) = Complex.abs (f z * (z ^ d)⁻¹ - 1)
Tactic:
rw [div_eq_mul_inv]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z * (z ^ d)⁻¹ - 1) = Complex.abs ((f z - z ^ d) * (z ^ d)⁻¹)
Tactic:
rw [mul_sub_right_distrib, mul_inv_cancel (pow_ne_zero d z0)]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs ((f z - z ^ d) * (z ^ d)⁻¹) = Complex.abs (f z - z ^ d) * (Complex.abs (z ^ d))⁻¹
Tactic:
rw [Complex.abs.map_mul, map_inv₀]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ Complex.abs (f z - z ^ d) * (Complex.abs (z ^ d))⁻¹ ≤ e / 2 * Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ e / 2 * Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹ = e / 2 * (Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹)
Tactic:
ring
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ e / 2 * (Complex.abs (z ^ d) * (Complex.abs (z ^ d))⁻¹) ≤ e / 2 * 1
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t✝¹ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t✝ : Set ℂ
o : IsOpen t✝
fa : AnalyticOn ℂ f t✝
ht : ball c r = t✝
ga : DifferentiableOn ℂ (g f d) (t✝ \ {0})
t0 : 0 ∈ t✝
e : ℝ
ep : e > 0
t : ℝ
tp : t > 0
z : ℂ
zs : dist z 0 < t
h : Complex.abs (f z - z ^ d) ≤ e / 2 * Complex.abs (z ^ d)
z0 : ¬z = 0
⊢ e / 2 * 1 = e / 2
Tactic:
ring
State after:
no goals