Theorem: Super.ray_noncritical (Ray/Dynamics/Ray.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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
by_cases x0 : x = 0
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
rw [x0]
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) 0 ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : x = 0
⊢ mfderiv I I (s.ray c) 0 ≠ 0

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
exact s.ray_noncritical_zero c
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
set n := s.np c (abs x)
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
⊢ mfderiv I I (s.ray c) x ≠ 0

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
have h : mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0 := by
  have e : s.bottcherNearIter n c ∘ s.ray c =ᶠ[𝓝 x] fun x ↦ x ^ d ^ n :=
    (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_iter post)
  rw [e.mfderiv_eq]; contrapose x0; simp only [not_not] at x0 ⊢
  rw [mfderiv_eq_fderiv] at x0
  have d := (differentiableAt_pow (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
  apply_fun (fun x ↦ x 1) at x0
  rw [x0] at d
  replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
  rw [deriv_pow, mul_eq_zero, Nat.cast_eq_zero, pow_eq_zero_iff', pow_eq_zero_iff'] at d
  simp only [s.d0, false_and_iff, false_or_iff] at d; exact d.1
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h : mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
⊢ mfderiv I I (s.ray c) x ≠ 0

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h : mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
simp only [mfderiv_comp x
    (s.bottcherNearIter_holomorphic (s.ray_near post)).along_snd.mdifferentiableAt
    (s.ray_holomorphic post).along_snd.mdifferentiableAt,
  Ne, mderiv_comp_eq_zero_iff, not_or] at h
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h :
  ¬mfderiv I I (fun y => s.bottcherNearIter (s.np c (Complex.abs x)) c y) (s.ray c x) = 0 ∧ ¬mfderiv I I (s.ray c) x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
h :
  ¬mfderiv I I (fun y => s.bottcherNearIter (s.np c (Complex.abs x)) c y) (s.ray c x) = 0 ∧ ¬mfderiv I I (s.ray c) x = 0
⊢ mfderiv I I (s.ray c) x ≠ 0
Tactic:
exact h.2
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
⊢ mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
Tactic:
have e : s.bottcherNearIter n c ∘ s.ray c =ᶠ[𝓝 x] fun x ↦ x ^ d ^ n :=
  (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_iter post)
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (s.bottcherNearIter n c ∘ s.ray c) x ≠ 0
Tactic:
rw [e.mfderiv_eq]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (fun x => x ^ d ^ n) x ≠ 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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
x0 : ¬x = 0
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
⊢ mfderiv I I (fun x => x ^ d ^ n) x ≠ 0
Tactic:
contrapose x0
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : ¬mfderiv I I (fun x => x ^ d ^ n) x ≠ 0
⊢ ¬¬x = 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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : ¬mfderiv I I (fun x => x ^ d ^ n) x ≠ 0
⊢ ¬¬x = 0
Tactic:
simp only [not_not] at x0 ⊢
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : mfderiv I I (fun x => x ^ d ^ n) x = 0
⊢ x = 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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : mfderiv I I (fun x => x ^ d ^ n) x = 0
⊢ x = 0
Tactic:
rw [mfderiv_eq_fderiv] at x0
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : fderiv ℂ (fun x => x ^ d ^ n) x = 0
⊢ x = 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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d ^ n
x0 : fderiv ℂ (fun x => x ^ d ^ n) x = 0
⊢ x = 0
Tactic:
have d := (differentiableAt_pow (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : fderiv ℂ (fun x => x ^ d✝ ^ n) x = 0
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
⊢ x = 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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : fderiv ℂ (fun x => x ^ d✝ ^ n) x = 0
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
⊢ x = 0
Tactic:
apply_fun (fun x ↦ x 1) at x0
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
rw [x0] at d
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : deriv (fun x => x ^ d✝ ^ n) x = 0
⊢ x = 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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : deriv (fun x => x ^ d✝ ^ n) x = 0
⊢ x = 0
Tactic:
rw [deriv_pow, mul_eq_zero, Nat.cast_eq_zero, pow_eq_zero_iff', pow_eq_zero_iff'] at d
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : d✝ = 0 ∧ n ≠ 0 ∨ x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : d✝ = 0 ∧ n ≠ 0 ∨ x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Tactic:
simp only [s.d0, false_and_iff, false_or_iff] at d
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 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 x : ℂ
a z : S
d✝ n✝ : ℕ
s✝ : Super f d✝ a
y : ℂ × ℂ
s : Super f d✝ a
inst✝ : OnePreimage s
post : (c, x) ∈ s.ext
n : ℕ := s.np c (Complex.abs x)
e : (𝓝 x).EventuallyEq (s.bottcherNearIter n c ∘ s.ray c) fun x => x ^ d✝ ^ n
x0 : (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1 = 0 1
d : x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Tactic:
exact d.1
State after:
no goals