Theorem: Super.bottcherNearIter_mfderiv_ne_zero (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
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬Precritical (f c) z
⊢ mfderiv I I (s.bottcherNearIter n c) z ≠ 0
Tactic:
apply mderiv_comp_ne_zero' b0
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
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬Precritical (f c) z
⊢ mfderiv I I (f c)^[n] z ≠ 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
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬Precritical (f c) z
⊢ mfderiv I I (f c)^[n] z ≠ 0
Tactic:
contrapose f0
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
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬mfderiv I I (f c)^[n] z ≠ 0
⊢ ¬¬Precritical (f c) 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
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬mfderiv I I (f c)^[n] z ≠ 0
⊢ ¬¬Precritical (f c) z
Tactic:
simp only [not_not] at f0 ⊢
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
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : mfderiv I I (f c)^[n] z = 0
⊢ Precritical (f c) 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
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : mfderiv I I (f c)^[n] z = 0
⊢ Precritical (f c) z
Tactic:
exact critical_iter s.fa.along_snd f0
State after:
no goals