Theorem: Super.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
⊢ (p.1, f p.1 p.2) ∈ s.post
Tactic:
rcases p with ⟨c, z⟩
State after:
case mk
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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ ((c, z).1, f (c, z).1 (c, z).2) ∈ s.post

State before:
case mk
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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ ((c, z).1, f (c, z).1 (c, z).2) ∈ s.post
Tactic:
simp only [Super.post, mem_setOf, Postcritical, s.potential_eqn]
State after:
case mk
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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ s.potential c z ^ d < s.p c

State before:
case mk
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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ s.potential c z ^ d < s.p c
Tactic:
exact lt_of_le_of_lt (pow_le_of_le_one s.potential_nonneg s.potential_le_one s.d0) m
State after:
no goals