Theorem: Super.critical_a (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 (f c) a
Tactic:
have h := s.critical_0 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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
h : Critical (s.fl c) 0
⊢ Critical (f 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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
h : Critical (s.fl c) 0
⊢ Critical (f c) a
Tactic:
have e := PartialEquiv.left_inv _ (mem_extChartAt_source I a)
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 : ℂ
h : Critical (s.fl c) 0
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
⊢ Critical (f 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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
h : Critical (s.fl c) 0
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
⊢ Critical (f c) a
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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : ¬Critical (f c) a
⊢ ¬Critical (s.fl c) 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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : ¬Critical (f c) a
⊢ ¬Critical (s.fl c) 0
Tactic:
simp only [Critical, Super.fl, fl, ← ne_eq] 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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (_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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (_root_.fl f a c) 0 ≠ 0
Tactic:
simp only [mfderiv_eq_fderiv, _root_.fl, Function.comp]
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ fderiv ℂ (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) - ↑(extChartAt I a) a)
      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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ fderiv ℂ (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) - ↑(extChartAt I a) a)
      0 ≠
    0
Tactic:
rw [fderiv_sub_const, ←mfderiv_eq_fderiv]
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)))) 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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a) (f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)))) 0 ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (extChartAt_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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) 0 ≠ 0

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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ f c (↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a)) ∈ (extChartAt I a).source

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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => f c (↑(extChartAt I a).symm (x + ↑(extChartAt I a) a))) 0 ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (f := f c)
State after:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) (↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a)) ≠ 0

case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0 ≠ 0

State before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) (↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a)) ≠ 0
Tactic:
rw [zero_add, e]
State after:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) a ≠ 0

State before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (f c) a ≠ 0
Tactic:
exact h
State after:
no goals

State before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => ↑(extChartAt I a).symm (x + ↑(extChartAt I a) a)) 0 ≠ 0
Tactic:
apply mderiv_comp_ne_zero' (extChartAt_symm_mderiv_ne_zero' ?_)
State after:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x + ↑(extChartAt I a) a) 0 ≠ 0

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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target

State before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x + ↑(extChartAt I a) a) 0 ≠ 0
Tactic:
rw [mfderiv_eq_fderiv, fderiv_add_const, ←mfderiv_eq_fderiv]
State after:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x) 0 ≠ 0

State before:
case a
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ mfderiv I I (fun x => x) 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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
c : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ 0 + ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
rw [zero_add]
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target

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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ ↑(extChartAt I a) a ∈ (extChartAt I a).target
Tactic:
apply mem_extChartAt_target
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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ f c (↑(extChartAt I a).symm (0 + ↑(extChartAt I a) a)) ∈ (extChartAt I a).source
Tactic:
simp only [zero_add, e, s.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
c : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ a ∈ (extChartAt I a).source

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 : ℂ
e : ↑(extChartAt I a).symm (↑(extChartAt I a) a) = a
h : mfderiv I I (f c) a ≠ 0
⊢ a ∈ (extChartAt I a).source
Tactic:
apply mem_extChartAt_source
State after:
no goals