Theorem: Super.iter_stays_post (Ray/Dynamics/Postcritical.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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
⊢ (p.1, (f p.1)^[n] p.2) ∈ s.post
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, (f p.1)^[0] p.2) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, (f p.1)^[0] p.2) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, p.2) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, p.2) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
Tactic:
exact m
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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, f p.1 ((f p.1)^[n] p.2)) ∈ s.post

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 z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, f p.1 ((f p.1)^[n] p.2)) ∈ s.post
Tactic:
exact s.stays_post h
State after:
no goals