Theorem: Super.iter_nontrivial_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
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
Tactic:
induction' n with n h
State after:
case zero
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
⊢ NontrivialHolomorphicAt (fun z => (f c)^[0] z) a

case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a

State before:
case zero
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
⊢ NontrivialHolomorphicAt (fun z => (f c)^[0] z) a

case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Tactic:
simp only [Function.iterate_zero_apply]
State after:
case zero
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
⊢ NontrivialHolomorphicAt (fun z => z) a

case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a

State before:
case zero
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
⊢ NontrivialHolomorphicAt (fun z => z) a

case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Tactic:
apply nontrivialHolomorphicAt_id
State after:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a

State before:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Tactic:
simp only [Function.iterate_succ_apply']
State after:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => f c ((f c)^[n] z)) a

State before:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => f c ((f c)^[n] z)) a
Tactic:
refine NontrivialHolomorphicAt.comp ?_ h
State after:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) ((f c)^[n] a)

State before:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) ((f c)^[n] a)
Tactic:
simp only [s.iter_a]
State after:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) a

State before:
case succ
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
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) a
Tactic:
exact s.f_nontrivial c
State after:
no goals