Theorem: Super.critical_0 (Ray/Dynamics/BottcherNearM.lean)

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ Critical (s.fl c) 0
Tactic:
simp only [Critical, mfderiv_eq_fderiv, Super.fl]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Tactic:
have p := (s.fla c).along_snd.leading_approx
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
p :
  (fun z =>
      uncurry s.fl ((c, 0).1, z) -
        (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 •
          leadingCoeff (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2) =o[𝓝 (c, 0).2]
    fun z => (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
p :
  (fun z =>
      uncurry s.fl ((c, 0).1, z) -
        (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2 •
          leadingCoeff (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2) =o[𝓝 (c, 0).2]
    fun z => (z - (c, 0).2) ^ orderAt (fun y => uncurry s.fl ((c, 0).1, y)) (c, 0).2
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Tactic:
simp only [sub_zero, Algebra.id.smul_eq_mul, Super.fl, s.fd, s.fc, mul_one, uncurry] at p
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
p : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
p : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ fderiv ℂ (_root_.fl f a c) 0 = 0
Tactic:
generalize hg : _root_.fl f a c = g
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
p : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
g : ℂ → ℂ
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
p : (fun z => _root_.fl f a c z - z ^ d) =o[𝓝 0] fun z => z ^ d
g : ℂ → ℂ
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0
Tactic:
rw [hg] at p
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ fderiv ℂ g 0 = 0
Tactic:
have g0 : g 0 = 0 := by rw [← hg]; exact s.fl0
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ fderiv ℂ g 0 = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ fderiv ℂ g 0 = 0
Tactic:
apply HasFDerivAt.fderiv
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ HasFDerivAt g 0 0

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ HasFDerivAt g 0 0
Tactic:
simp only [hasFDerivAt_iff_isLittleO_nhds_zero, ContinuousLinearMap.zero_apply, sub_zero,
  zero_add, g0]
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
have od : (fun z : ℂ ↦ z ^ d) =o[𝓝 0] (fun z ↦ z) := by
  rw [Asymptotics.isLittleO_iff]; intro e ep
  apply ((@Metric.isOpen_ball ℂ _ 0 (min 1 e)).eventually_mem (mem_ball_self (by bound))).mp
  refine eventually_of_forall fun z b ↦ ?_
  simp only at b; rw [mem_ball_zero_iff, Complex.norm_eq_abs, lt_min_iff] at b
  simp only [Complex.norm_eq_abs, Complex.abs.map_pow]
  rw [← Nat.sub_add_cancel s.d2, pow_add, pow_two]
  calc abs z ^ (d - 2) * (abs z * abs z)
    _ ≤ (1:ℝ) ^ (d - 2) * (abs z * abs z) := by bound
    _ = abs z * abs z := by simp only [one_pow, one_mul]
    _ ≤ e * abs z := by bound
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
have p' := (p.trans od).add od
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x - x ^ d + x ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x - x ^ d + x ^ d) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
simp only [sub_add_cancel] at p'
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ (fun h => g h - 0 h) =o[𝓝 0] fun h => h
Tactic:
refine p'.congr_left ?_
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ ∀ (x : ℂ), g x = g x - 0 x

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
⊢ ∀ (x : ℂ), g x = g x - 0 x
Tactic:
intro z
State after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
z : ℂ
⊢ g z = g z - 0 z

State before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
od : (fun z => z ^ d) =o[𝓝 0] fun z => z
p' : (fun x => g x) =o[𝓝 0] fun z => z
z : ℂ
⊢ g z = g z - 0 z
Tactic:
exact (sub_zero _).symm
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ g 0 = 0
Tactic:
rw [← hg]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ _root_.fl f a c 0 = 0

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
⊢ _root_.fl f a c 0 = 0
Tactic:
exact s.fl0
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ (fun z => z ^ d) =o[𝓝 0] fun z => z
Tactic:
rw [Asymptotics.isLittleO_iff]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ c * ‖x‖

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ c * ‖x‖
Tactic:
intro e ep
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ e * ‖x‖

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖x ^ d‖ ≤ e * ‖x‖
Tactic:
apply ((@Metric.isOpen_ball ℂ _ 0 (min 1 e)).eventually_mem (mem_ball_self (by bound))).mp
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ ball 0 (min 1 e) → ‖x ^ d‖ ≤ e * ‖x‖

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ ball 0 (min 1 e) → ‖x ^ d‖ ≤ e * ‖x‖
Tactic:
refine eventually_of_forall fun z b ↦ ?_
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : z ∈ ball 0 (min 1 e)
⊢ ‖z ^ d‖ ≤ e * ‖z‖

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : z ∈ ball 0 (min 1 e)
⊢ ‖z ^ d‖ ≤ e * ‖z‖
Tactic:
rw [mem_ball_zero_iff, Complex.norm_eq_abs, lt_min_iff] at b
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ ‖z ^ d‖ ≤ e * ‖z‖

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ ‖z ^ d‖ ≤ e * ‖z‖
Tactic:
simp only [Complex.norm_eq_abs, Complex.abs.map_pow]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ d ≤ e * Complex.abs z

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ d ≤ e * Complex.abs z
Tactic:
rw [← Nat.sub_add_cancel s.d2, pow_add, pow_two]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ (d - 2) * (Complex.abs z * Complex.abs z) ≤ e * Complex.abs z

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ (d - 2) * (Complex.abs z * Complex.abs z) ≤ e * Complex.abs z
Tactic:
calc abs z ^ (d - 2) * (abs z * abs z)
  _ ≤ (1:ℝ) ^ (d - 2) * (abs z * abs z) := by bound
  _ = abs z * abs z := by simp only [one_pow, one_mul]
  _ ≤ e * abs z := by bound
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
⊢ 0 < min 1 e
Tactic:
bound
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z ^ (d - 2) * (Complex.abs z * Complex.abs z) ≤ 1 ^ (d - 2) * (Complex.abs z * Complex.abs z)
Tactic:
bound
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ 1 ^ (d - 2) * (Complex.abs z * Complex.abs z) = Complex.abs z * Complex.abs z
Tactic:
simp only [one_pow, one_mul]
State after:
no goals

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
g : ℂ → ℂ
p : (fun z => g z - z ^ d) =o[𝓝 0] fun z => z ^ d
hg : _root_.fl f a c = g
g0 : g 0 = 0
e : ℝ
ep : 0 < e
z : ℂ
b : Complex.abs z < 1 ∧ Complex.abs z < e
⊢ Complex.abs z * Complex.abs z ≤ e * Complex.abs z
Tactic:
bound
State after:
no goals