Theorem: df_ne_zero (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), deriv (f p.1) p.2 = 0 ↔ p.2 = 0
Tactic:
have df : ∀ e z, (e, z) ∈ t →
    deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z := by
  intro e z m; apply HasDerivAt.deriv
  have fg : f e = fun z ↦ z ^ d * g (f e) d z := by funext; rw [(s.ts m).fg]
  nth_rw 1 [fg]
  apply HasDerivAt.mul; apply hasDerivAt_pow
  rw [hasDerivAt_deriv_iff]; exact ((s.ts m).ga _ m).differentiableAt
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), deriv (f p.1) p.2 = 0 ↔ p.2 = 0

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), deriv (f p.1) p.2 = 0 ↔ p.2 = 0
Tactic:
apply small.mp
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
apply (s.o.eventually_mem (s.s m).t0).mp
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    x ∈ t →
      Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) →
        (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    x ∈ t →
      Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) →
        (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
apply Filter.eventually_of_forall
State after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)

State before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
clear small
State after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)

State before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ x ∈ t,
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
intro ⟨e, w⟩ m' small
State after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs ((e, w).2 * deriv (g (f (e, w).1) d) (e, w).2) < Complex.abs (↑d * g (f (e, w).1) d (e, w).2)
⊢ deriv (f (e, w).1) (e, w).2 = 0 ↔ (e, w).2 = 0

State before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs ((e, w).2 * deriv (g (f (e, w).1) d) (e, w).2) < Complex.abs (↑d * g (f (e, w).1) d (e, w).2)
⊢ deriv (f (e, w).1) (e, w).2 = 0 ↔ (e, w).2 = 0
Tactic:
simp only [df _ _ m'] at small ⊢
State after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ d * deriv (g (f e) d) w = 0 ↔ w = 0

State before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ d * deriv (g (f e) d) w = 0 ↔ w = 0
Tactic:
nth_rw 4 [← Nat.sub_add_cancel (Nat.succ_le_of_lt (s.s m).dp)]
State after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ (d - Nat.succ 0 + Nat.succ 0) * deriv (g (f e) d) w = 0 ↔ w = 0

State before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ ↑d * w ^ (d - 1) * g (f e) d w + w ^ (d - Nat.succ 0 + Nat.succ 0) * deriv (g (f e) d) w = 0 ↔ w = 0
Tactic:
simp only [pow_add, pow_one, mul_comm _ (w ^ (d - 1)), mul_assoc (w ^ (d - 1)) _ _, ←
  left_distrib, mul_eq_zero, pow_eq_zero_iff (Nat.sub_pos_of_lt (s.s m).d2).ne']
State after:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ w = 0 ∨ ↑d * g (f e) d w + w * deriv (g (f e) d) w = 0 ↔ w = 0

State before:
case hp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
e w : ℂ
m' : (e, w) ∈ t
small : Complex.abs (w * deriv (g (f e) d) w) < Complex.abs (↑d * g (f e) d w)
⊢ w = 0 ∨ ↑d * g (f e) d w + w * deriv (g (f e) d) w = 0 ↔ w = 0
Tactic:
exact or_iff_left (add_ne_zero_of_abs_lt small)
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
Tactic:
intro e z m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
Tactic:
apply HasDerivAt.deriv
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Tactic:
have fg : f e = fun z ↦ z ^ d * g (f e) d z := by funext; rw [(s.ts m).fg]
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (f e) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Tactic:
nth_rw 1 [fg]
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun z => z ^ d * g (f e) d z) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun z => z ^ d * g (f e) d z) (↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z) z
Tactic:
apply HasDerivAt.mul
State after:
case h.hc
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => y ^ d) (↑d * z ^ (d - 1)) z

case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z

State before:
case h.hc
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => y ^ d) (↑d * z ^ (d - 1)) z

case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z
Tactic:
apply hasDerivAt_pow
State after:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z

State before:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ HasDerivAt (fun y => g (f e) d y) (deriv (g (f e) d) z) z
Tactic:
rw [hasDerivAt_deriv_iff]
State after:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ DifferentiableAt ℂ (fun y => g (f e) d y) z

State before:
case h.hd
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
fg : f e = fun z => z ^ d * g (f e) d z
⊢ DifferentiableAt ℂ (fun y => g (f e) d y) z
Tactic:
exact ((s.ts m).ga _ m).differentiableAt
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
⊢ f e = fun z => z ^ d * g (f e) d z
Tactic:
funext
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
x✝ : ℂ
⊢ f e x✝ = x✝ ^ d * g (f e) d x✝

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m✝ : c ∈ u
e z : ℂ
m : (e, z) ∈ t
x✝ : ℂ
⊢ f e x✝ = x✝ ^ d * g (f e) d x✝
Tactic:
rw [(s.ts m).fg]
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
Tactic:
have ga : AnalyticAt ℂ (uncurry fun c z ↦ g (f c) d z) (c, 0) := s.ga _ (s.s m).t0
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
Tactic:
apply ContinuousAt.eventually_lt
State after:
case hf
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (x.2 * deriv (g (f x.1) d) x.2)) (c, 0)

case hg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (↑d * g (f x.1) d x.2)) (c, 0)

case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ Complex.abs ((c, 0).2 * deriv (g (f (c, 0).1) d) (c, 0).2) < Complex.abs (↑d * g (f (c, 0).1) d (c, 0).2)

State before:
case hf
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (x.2 * deriv (g (f x.1) d) x.2)) (c, 0)
Tactic:
exact Complex.continuous_abs.continuousAt.comp (continuousAt_snd.mul ga.deriv2.continuousAt)
State after:
no goals

State before:
case hg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ ContinuousAt (fun x => Complex.abs (↑d * g (f x.1) d x.2)) (c, 0)
Tactic:
exact Complex.continuous_abs.continuousAt.comp (continuousAt_const.mul ga.continuousAt)
State after:
no goals

State before:
case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ Complex.abs ((c, 0).2 * deriv (g (f (c, 0).1) d) (c, 0).2) < Complex.abs (↑d * g (f (c, 0).1) d (c, 0).2)
Tactic:
simp only [g0, MulZeroClass.zero_mul, Complex.abs.map_zero, Complex.abs.map_mul,
  Complex.abs_natCast, Complex.abs.map_one, mul_one, Nat.cast_pos]
State after:
case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ 0 < d

State before:
case hfg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
ga : AnalyticAt ℂ (uncurry fun c z => g (f c) d z) (c, 0)
⊢ 0 < d
Tactic:
exact (s.s m).dp
State after:
no goals