Theorem: Super.isClosed_critical_not_a (Ray/Dynamics/BottcherNearM.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 : S
d n : ℕ
s : Super f d a
⊢ IsClosed {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}
Tactic:
rw [← isOpen_compl_iff]
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 : S
d n : ℕ
s : Super f d a
⊢ IsOpen {p | Critical (f p.1) p.2 ∧ p.2 ≠ 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 : S
d n : ℕ
s : Super f d a
⊢ IsOpen {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
rw [isOpen_iff_eventually]
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 : S
d n : ℕ
s : Super f d a
⊢ ∀ x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ 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 : S
d n : ℕ
s : Super f d a
⊢ ∀ x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
intro ⟨c, z⟩ m
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ 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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
by_cases za : z = a
State after:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ

case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ

State before:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
rw [za]
State after:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, a), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ

State before:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, a), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
refine (s.f_noncritical_near_a c).mp (eventually_of_forall ?_)
State after:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ (x : ℂ × S), (Critical (f x.1) x.2 ↔ x.2 = a) → x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ

State before:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
⊢ ∀ (x : ℂ × S), (Critical (f x.1) x.2 ↔ x.2 = a) → x ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
intro ⟨e, w⟩ h
State after:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f (e, w).1) (e, w).2 ↔ (e, w).2 = a
⊢ (e, w) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ

State before:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f (e, w).1) (e, w).2 ↔ (e, w).2 = a
⊢ (e, w) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
simp only [mem_compl_iff, mem_setOf, not_and, not_not] at h ⊢
State after:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f e) w ↔ w = a
⊢ Critical (f e) w → w = a

State before:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : z = a
e : ℂ
w : S
h : Critical (f e) w ↔ w = a
⊢ Critical (f e) w → w = a
Tactic:
exact h.1
State after:
no goals

State before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
have o := isOpen_iff_eventually.mp (isOpen_noncritical s.fa)
State after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
o : ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ

State before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
za : ¬z = a
o : ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | Critical (f p.1) p.2 ∧ p.2 ≠ a}ᶜ
Tactic:
simp only [za, mem_compl_iff, mem_setOf, not_and, not_not, imp_false] at m o ⊢
State after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), Critical (f y.1) y.2 → y.2 = a

State before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), Critical (f y.1) y.2 → y.2 = a
Tactic:
refine (o (c, z) m).mp (eventually_of_forall ?_)
State after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → Critical (f x.1) x.2 → x.2 = a

State before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → Critical (f x.1) x.2 → x.2 = a
Tactic:
intro ⟨e, w⟩ a b
State after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ (e, w).2 = a✝

State before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ (e, w).2 = a✝
Tactic:
exfalso
State after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ False

State before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ False
Tactic:
exact a b
State after:
no goals