Theorem: critical_iter (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
n : ℕ
z : S
fa : Holomorphic I I f
c : Critical f^[n] z
⊢ Precritical f z
Tactic:
induction' n with n h
State after:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
c : Critical f^[0] z
⊢ Precritical f z

case succ
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : Critical f^[n + 1] z
⊢ Precritical f z

State before:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
c : Critical f^[0] z
⊢ Precritical f z
Tactic:
rw [Function.iterate_zero, Critical, mfderiv_id, ← ContinuousLinearMap.opNorm_zero_iff,
  ContinuousLinearMap.norm_id] at c
State after:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
c : 1 = 0
⊢ Precritical f z

State before:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
c : 1 = 0
⊢ Precritical f z
Tactic:
norm_num at c
State after:
no goals

State before:
case succ
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : Critical f^[n + 1] z
⊢ Precritical f z
Tactic:
rw [Function.iterate_succ', Critical,
  mfderiv_comp z (fa _).mdifferentiableAt (fa.iter _ _).mdifferentiableAt,
  mderiv_comp_eq_zero_iff] at c
State after:
case succ
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0 ∨ mfderiv I I f^[n] z = 0
⊢ Precritical f z

State before:
case succ
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0 ∨ mfderiv I I f^[n] z = 0
⊢ Precritical f z
Tactic:
cases' c with c c
State after:
case succ.inl
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0
⊢ Precritical f z

case succ.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z

State before:
case succ.inl
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f (f^[n] z) = 0
⊢ Precritical f z

case succ.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z
Tactic:
use n, c
State after:
case succ.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z

State before:
case succ.inr
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S → S
z : S
fa : Holomorphic I I f
n : ℕ
h : Critical f^[n] z → Precritical f z
c : mfderiv I I f^[n] z = 0
⊢ Precritical f z
Tactic:
exact h c
State after:
no goals