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
za : z ≠ a
inst✝ : OnePreimage s
⊢ ¬Precritical (f c) z
Tactic:
apply p.not_precritical
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
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ s.potential c 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
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ s.potential c z ≠ 0
Tactic:
simp only [Ne, s.potential_eq_zero_of_onePreimage]
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
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ ¬z = a

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
za : z ≠ a
inst✝ : OnePreimage s
⊢ ¬z = a
Tactic:
exact za
State after:
no goals