Theorem: Super.no_jump (Ray/Dynamics/Potential.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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
Tactic:
have h : ∀ q : ℂ × S, f q.1 q.2 = a → q.2 = a := fun _ ↦ by simp only [s.preimage_eq', imp_self]
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n

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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
Tactic:
contrapose h
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ¬∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ¬∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
simp only [Filter.not_eventually, not_forall, exists_prop] at h
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
set t := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
have tc : IsClosed t := by
  refine (IsCompact.image ?_ s.fpa.continuous).isClosed
  exact ((isCompact_closedBall _ _).prod isCompact_univ).inter_right no.isClosed_compl
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
have th : ∃ᶠ p in 𝓝 (c, a), p ∈ t := by
  have mb : ∀ᶠ p : ℂ × S in 𝓝 (c, a), p.1 ∈ closedBall c 1 :=
    continuousAt_fst.eventually_mem_nhd (Metric.closedBall_mem_nhds _ zero_lt_one)
  refine (h.and_eventually mb).mp (eventually_of_forall fun p i ↦ ?_)
  rcases i with ⟨⟨q, qp, m⟩, b⟩
  simp only [Prod.ext_iff] at qp; simp only [qp.1] at b
  simp only [Set.mem_image, Set.mem_compl_iff, Set.mem_inter_iff, Set.mem_prod_eq, Set.mem_univ,
    and_true_iff, Prod.ext_iff, t]
  use q, ⟨b, m⟩, qp.1.symm, qp.2.symm
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
have m := th.mem_of_closed tc
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m : (c, a) ∈ t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m : (c, a) ∈ t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
rcases(Set.mem_image _ _ _).mp m with ⟨p, m, pa⟩
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : s.fp p = (c, a)
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : s.fp p = (c, a)
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
simp only [Super.fp, Prod.mk.inj_iff] at pa
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : p.1 = c ∧ f p.1 p.2 = a
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : p.1 = c ∧ f p.1 p.2 = a
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
simp only [not_forall]
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : p.1 = c ∧ f p.1 p.2 = a
⊢ ∃ x, ∃ (_ : f x.1 x.2 = a), ¬x.2 = a

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : p.1 = c ∧ f p.1 p.2 = a
⊢ ∃ x, ∃ (_ : f x.1 x.2 = a), ¬x.2 = a
Tactic:
use p, pa.2
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : p.1 = c ∧ f p.1 p.2 = a
⊢ ¬p.2 = a

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
m : p ∈ closedBall c 1 ×ˢ univ ∩ nᶜ
pa : p.1 = c ∧ f p.1 p.2 = a
⊢ ¬p.2 = a
Tactic:
contrapose m
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
pa : p.1 = c ∧ f p.1 p.2 = a
m : ¬¬p.2 = a
⊢ p ∉ closedBall c 1 ×ˢ univ ∩ nᶜ

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
pa : p.1 = c ∧ f p.1 p.2 = a
m : ¬¬p.2 = a
⊢ p ∉ closedBall c 1 ×ˢ univ ∩ nᶜ
Tactic:
simp only [not_not, Set.mem_compl_iff] at m ⊢
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
pa : p.1 = c ∧ f p.1 p.2 = a
m : p.2 = a
⊢ p ∉ closedBall c 1 ×ˢ univ ∩ nᶜ

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
pa : p.1 = c ∧ f p.1 p.2 = a
m : p.2 = a
⊢ p ∉ closedBall c 1 ×ˢ univ ∩ nᶜ
Tactic:
rw [← @Prod.mk.eta _ _ p, pa.1, m]
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
pa : p.1 = c ∧ f p.1 p.2 = a
m : p.2 = a
⊢ (c, a) ∉ closedBall c 1 ×ˢ univ ∩ nᶜ

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m✝ : (c, a) ∈ t
p : ℂ × S
pa : p.1 = c ∧ f p.1 p.2 = a
m : p.2 = a
⊢ (c, a) ∉ closedBall c 1 ×ˢ univ ∩ nᶜ
Tactic:
simp only [Set.mem_inter_iff, Set.prod_mk_mem_set_prod_eq, Metric.mem_closedBall, dist_self,
  zero_le_one, Set.mem_univ, Set.mem_compl_iff, true_and_iff, Set.not_not_mem, not_not,
  na]
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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
x✝ : ℂ × S
⊢ f x✝.1 x✝.2 = a → x✝.2 = a
Tactic:
simp only [s.preimage_eq', imp_self]
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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
⊢ IsClosed t
Tactic:
refine (IsCompact.image ?_ s.fpa.continuous).isClosed
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
⊢ IsCompact (closedBall c 1 ×ˢ univ ∩ nᶜ)

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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
⊢ IsCompact (closedBall c 1 ×ˢ univ ∩ nᶜ)
Tactic:
exact ((isCompact_closedBall _ _).prod isCompact_univ).inter_right no.isClosed_compl
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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
⊢ ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
Tactic:
have mb : ∀ᶠ p : ℂ × S in 𝓝 (c, a), p.1 ∈ closedBall c 1 :=
  continuousAt_fst.eventually_mem_nhd (Metric.closedBall_mem_nhds _ zero_lt_one)
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
⊢ ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t

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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
⊢ ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
Tactic:
refine (h.and_eventually mb).mp (eventually_of_forall fun p i ↦ ?_)
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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p : ℂ × S
i : (∃ x, p = s.fp x ∧ x ∉ n) ∧ p.1 ∈ closedBall c 1
⊢ p ∈ t

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
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p : ℂ × S
i : (∃ x, p = s.fp x ∧ x ∉ n) ∧ p.1 ∈ closedBall c 1
⊢ p ∈ t
Tactic:
rcases i with ⟨⟨q, qp, m⟩, b⟩
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p : ℂ × S
b : p.1 ∈ closedBall c 1
q : ℂ × S
qp : p = s.fp q
m : q ∉ n
⊢ p ∈ t

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p : ℂ × S
b : p.1 ∈ closedBall c 1
q : ℂ × S
qp : p = s.fp q
m : q ∉ n
⊢ p ∈ t
Tactic:
simp only [Prod.ext_iff] at qp
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p : ℂ × S
b : p.1 ∈ closedBall c 1
q : ℂ × S
m : q ∉ n
qp : p.1 = (s.fp q).1 ∧ p.2 = (s.fp q).2
⊢ p ∈ t

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p : ℂ × S
b : p.1 ∈ closedBall c 1
q : ℂ × S
m : q ∉ n
qp : p.1 = (s.fp q).1 ∧ p.2 = (s.fp q).2
⊢ p ∈ t
Tactic:
simp only [qp.1] at b
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p q : ℂ × S
m : q ∉ n
qp : p.1 = (s.fp q).1 ∧ p.2 = (s.fp q).2
b : (s.fp q).1 ∈ closedBall c 1
⊢ p ∈ t

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p q : ℂ × S
m : q ∉ n
qp : p.1 = (s.fp q).1 ∧ p.2 = (s.fp q).2
b : (s.fp q).1 ∈ closedBall c 1
⊢ p ∈ t
Tactic:
simp only [Set.mem_image, Set.mem_compl_iff, Set.mem_inter_iff, Set.mem_prod_eq, Set.mem_univ,
  and_true_iff, Prod.ext_iff, t]
State after:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p q : ℂ × S
m : q ∉ n
qp : p.1 = (s.fp q).1 ∧ p.2 = (s.fp q).2
b : (s.fp q).1 ∈ closedBall c 1
⊢ ∃ x, (x.1 ∈ closedBall c 1 ∧ x ∉ n) ∧ (s.fp x).1 = p.1 ∧ (s.fp x).2 = p.2

State before:
case 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 : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
mb : ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), p.1 ∈ closedBall c 1
p q : ℂ × S
m : q ∉ n
qp : p.1 = (s.fp q).1 ∧ p.2 = (s.fp q).2
b : (s.fp q).1 ∈ closedBall c 1
⊢ ∃ x, (x.1 ∈ closedBall c 1 ∧ x ∉ n) ∧ (s.fp x).1 = p.1 ∧ (s.fp x).2 = p.2
Tactic:
use q, ⟨b, m⟩, qp.1.symm, qp.2.symm
State after:
no goals