Theorem: Postcritical.not_precritical (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 : Super f d a
p : Postcritical s c z
p0 : s.potential c z ≠ 0
⊢ ¬Precritical (f c) z
Tactic:
contrapose p
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 z0 z1 : S
d n : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
p : ¬¬Precritical (f c) z
⊢ ¬Postcritical s c z

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 : Super f d a
p0 : s.potential c z ≠ 0
p : ¬¬Precritical (f c) z
⊢ ¬Postcritical s c z
Tactic:
simp only [Postcritical, not_not, not_forall, not_lt] at p ⊢
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 z0 z1 : S
d n : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
p : Precritical (f c) z
⊢ s.p c ≤ s.potential c z

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 : Super f d a
p0 : s.potential c z ≠ 0
p : Precritical (f c) z
⊢ s.p c ≤ s.potential c z
Tactic:
rcases p with ⟨n, p⟩
State after:
case intro
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c z

State before:
case intro
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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c z
Tactic:
trans s.potential c ((f c)^[n] z)
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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c ((f c)^[n] z)

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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≤ s.potential c z

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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.p c ≤ s.potential c ((f c)^[n] z)
Tactic:
refine csInf_le s.bddBelow_ps (Or.inr ⟨?_, (f c)^[n] z, rfl, p⟩)
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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≠ 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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≠ 0
Tactic:
simp only [s.potential_eqn_iter]
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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≠ 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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≠ 0
Tactic:
exact pow_ne_zero _ p0
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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c ((f c)^[n] z) ≤ s.potential c z
Tactic:
simp only [s.potential_eqn_iter]
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 z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≤ s.potential c z

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 : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≤ s.potential c z
Tactic:
exact pow_le_of_le_one s.potential_nonneg s.potential_le_one (pow_ne_zero _ s.d0)
State after:
no goals