Theorem: Super.ps_pos (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
c : ℂ
p : ℝ
m : p ∈ s.ps c
⊢ 0 < p
Tactic:
cases' m with m m
State after:
case inl
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 : ℂ
p : ℝ
m : p = 1
⊢ 0 < p

case inr
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 : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p

State before:
case inl
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 : ℂ
p : ℝ
m : p = 1
⊢ 0 < p

case inr
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 : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p
Tactic:
simp only [m, zero_lt_one]
State after:
case inr
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 : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p

State before:
case inr
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 : ℂ
p : ℝ
m : p ≠ 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
⊢ 0 < p
Tactic:
rcases m with ⟨p0, z, e, c⟩
State after:
case inr.intro.intro.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✝ s : Super f d a
c✝ : ℂ
p : ℝ
p0 : p ≠ 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < p

State before:
case inr.intro.intro.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✝ s : Super f d a
c✝ : ℂ
p : ℝ
p0 : p ≠ 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < p
Tactic:
rw [← e] at p0 ⊢
State after:
case inr.intro.intro.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✝ s : Super f d a
c✝ : ℂ
p : ℝ
z : S
p0 : s.potential c✝ z ≠ 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < s.potential c✝ z

State before:
case inr.intro.intro.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✝ s : Super f d a
c✝ : ℂ
p : ℝ
z : S
p0 : s.potential c✝ z ≠ 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ 0 < s.potential c✝ z
Tactic:
exact p0.symm.lt_of_le s.potential_nonneg
State after:
no goals