Theorem: Super.compact_ps (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
inst✝ : OnePreimage s
⊢ IsCompact (s.ps c)
Tactic:
have pc : Continuous (s.potential c) := (Continuous.potential s).along_snd
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✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
⊢ IsCompact (s.ps c)

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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
⊢ IsCompact (s.ps c)
Tactic:
have c1 : IsCompact {(1 : ℝ)} := isCompact_singleton
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✝ s : Super f d a
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ IsCompact (s.ps c)

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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ IsCompact (s.ps c)
Tactic:
convert c1.union ((s.isClosed_critical_not_a.snd_preimage c).isCompact.image pc)
State after:
case h.e'_3
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ s.ps c = {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}

State before:
case h.e'_3
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ s.ps c = {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Tactic:
apply Set.ext
State after:
case h.e'_3.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ ∀ (x : ℝ), x ∈ s.ps c ↔ x ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}

State before:
case h.e'_3.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
⊢ ∀ (x : ℝ), x ∈ s.ps c ↔ x ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Tactic:
intro p
State after:
case h.e'_3.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ p ∈ s.ps c ↔ p ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}

State before:
case h.e'_3.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ p ∈ s.ps c ↔ p ∈ {1} ∪ s.potential c '' {b | (c, b) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}}
Tactic:
simp only [mem_setOf, Super.ps, mem_singleton_iff, mem_union, mem_image, Ne, ←
  s.potential_eq_zero_of_onePreimage c]
State after:
case h.e'_3.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    p = 1 ∨ ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p

State before:
case h.e'_3.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (p = 1 ∨ ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    p = 1 ∨ ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p
Tactic:
apply or_congr_right
State after:
case h.e'_3.h.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p

State before:
case h.e'_3.h.h
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) ↔
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p
Tactic:
constructor
State after:
case h.e'_3.h.h.mp
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) →
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p

case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z

State before:
case h.e'_3.h.h.mp
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z) →
    ∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p

case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
intro ⟨p0, z, e, c⟩
State after:
case h.e'_3.h.h.mp
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
p0 : ¬p = 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z

State before:
case h.e'_3.h.h.mp
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
p0 : ¬p = 0
z : S
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
rw [← e] at p0
State after:
case h.e'_3.h.h.mp
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z

State before:
case h.e'_3.h.h.mp
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
c : Critical (f c✝) z
⊢ ∃ x, (Critical (f c✝) x ∧ ¬s.potential c✝ x = 0) ∧ s.potential c✝ x = p

case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
exact ⟨z, ⟨c, p0⟩, e⟩
State after:
case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z

State before:
case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c)
c1 : IsCompact {1}
p : ℝ
⊢ (∃ x, (Critical (f c) x ∧ ¬s.potential c x = 0) ∧ s.potential c x = p) →
    ¬p = 0 ∧ ∃ z, s.potential c z = p ∧ Critical (f c) z
Tactic:
intro ⟨z, ⟨c, p0⟩, e⟩
State after:
case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z

State before:
case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬s.potential c✝ z = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z
Tactic:
rw [e] at p0
State after:
case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬p = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z

State before:
case h.e'_3.h.h.mpr
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
inst✝ : OnePreimage s
pc : Continuous (s.potential c✝)
c1 : IsCompact {1}
p : ℝ
z : S
c : Critical (f c✝) z
p0 : ¬p = 0
e : s.potential c✝ z = p
⊢ ¬p = 0 ∧ ∃ z, s.potential c✝ z = p ∧ Critical (f c✝) z
Tactic:
exact ⟨p0, z, e, c⟩
State after:
no goals