Theorem: Super.ray_noncritical_zero (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
c : ℂ
⊢ mfderiv I I (s.ray c) 0 ≠ 0
Tactic:
have h : mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0 := by
  have e : s.bottcherNear c ∘ s.ray c =ᶠ[𝓝 0] id :=
    (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_zero c)
  rw [e.mfderiv_eq]; exact id_mderiv_ne_zero
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
c : ℂ
h : mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
⊢ mfderiv I I (s.ray 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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
⊢ mfderiv I I (s.ray c) 0 ≠ 0
Tactic:
contrapose h
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
c : ℂ
h : ¬mfderiv I I (s.ray c) 0 ≠ 0
⊢ ¬mfderiv I I (s.bottcherNear c ∘ s.ray 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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : ¬mfderiv I I (s.ray c) 0 ≠ 0
⊢ ¬mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
Tactic:
simp only [not_not] at h ⊢
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
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray 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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Tactic:
have hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0) := by
  rw [s.ray_zero]; exact (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd.mdifferentiableAt
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
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray 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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Tactic:
have hr : MDifferentiableAt I I (s.ray c) 0 :=
  (s.ray_holomorphic (s.mem_ext c)).along_snd.mdifferentiableAt
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
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
hr : MDifferentiableAt I I (s.ray c) 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray 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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
hb : MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
hr : MDifferentiableAt I I (s.ray c) 0
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 = 0
Tactic:
rw [mfderiv_comp 0 hb hr, h, ContinuousLinearMap.comp_zero]
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
c : ℂ
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 0
Tactic:
have e : s.bottcherNear c ∘ s.ray c =ᶠ[𝓝 0] id :=
  (continuousAt_const.prod continuousAt_id).eventually (s.ray_eqn_zero c)
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
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray 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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I (s.bottcherNear c ∘ s.ray c) 0 ≠ 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
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I id 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✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : (𝓝 0).EventuallyEq (s.bottcherNear c ∘ s.ray c) id
⊢ mfderiv I I id 0 ≠ 0
Tactic:
exact id_mderiv_ne_zero
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
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ MDifferentiableAt I I (s.bottcherNear c) (s.ray c 0)
Tactic:
rw [s.ray_zero]
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
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ MDifferentiableAt I I (s.bottcherNear c) a

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
c : ℂ
h : mfderiv I I (s.ray c) 0 = 0
⊢ MDifferentiableAt I I (s.bottcherNear c) a
Tactic:
exact (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd.mdifferentiableAt
State after:
no goals