internlm/Lean-Github huggingface dataset:
Theorem: Super.no_jump
Proof 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⟩
Proof 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
Theorem: Super.no_jump
Proof 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
Proof 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
Theorem: Super.no_jump
Proof 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]
Proof 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
Theorem: Super.no_jump
Proof 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
Proof 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
Theorem: Super.no_jump
Proof 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
Proof 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ᶜ
Theorem: Super.no_jump
Proof 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 ⊢
Proof 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ᶜ
Theorem: Super.no_jump
Proof 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]
Proof 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ᶜ
Theorem: Super.no_jump
Proof 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]
Proof state after:
no goals
Theorem: Super.no_jump
Proof 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]
Proof state after:
no goals
Theorem: Super.no_jump
Proof 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
Proof 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ᶜ)
Theorem: Super.no_jump
Proof 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
Proof state after:
no goals
Theorem: Super.no_jump
Proof 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)
Proof 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
Theorem: Super.no_jump
Proof 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 ↦ ?_)
Proof 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
Theorem: Super.no_jump
Proof 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⟩
Proof 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
Theorem: Super.no_jump
Proof 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
Proof 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
Theorem: Super.no_jump
Proof 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
Proof 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
Theorem: Super.no_jump
Proof 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]
Proof 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
Theorem: Super.no_jump
Proof 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
Proof state after:
no goals
Theorem: Super.barrier
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
⊢ ∃ t, Barrier s c n t
Tactic:
set n' := n ∩ s.near
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
⊢ ∃ t, Barrier s c n t
Theorem: Super.barrier
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
⊢ ∃ t, Barrier s c n t
Tactic:
have nn' : n' ∈ 𝓝 (c, a) :=
  Filter.inter_mem (no.mem_nhds na) (s.isOpen_near.mem_nhds (s.mem_near c))
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
⊢ ∃ t, Barrier s c n t
Theorem: Super.barrier
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
⊢ ∃ t, Barrier s c n t
Tactic:
rcases (Filter.hasBasis_iff.mp (compact_basis_nhds (c, a)) n').mp nn' with ⟨u, ⟨un, uc⟩, us⟩
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
us : u ⊆ n'
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
⊢ ∃ t, Barrier s c n t
Theorem: Super.barrier
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
us : u ⊆ n'
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
⊢ ∃ t, Barrier s c n t
Tactic:
simp only [Set.subset_inter_iff, n'] at us
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n ∧ u ⊆ s.near
⊢ ∃ t, Barrier s c n t
Theorem: Super.barrier
Proof 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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n ∧ u ⊆ s.near
⊢ ∃ t, Barrier s c n t
Tactic:
rcases eventually_nhds_iff.mp
    (s.no_jump c (interior u) isOpen_interior (mem_interior_iff_mem_nhds.mpr un)) with
  ⟨i, ih, io, ia⟩
Proof state after:
case intro.intro.intro.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
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
n' : Set (ℂ × S) := n ∩ s.near
nn' : n' ∈ 𝓝 (c, a)
u : Set (ℂ × S)
un : u ∈ 𝓝 (c, a)
uc : IsCompact u
us : u ⊆ n ∧ u ⊆ s.near
i : Set (ℂ × S)
ih : ∀ x ∈ i, ∀ (q : ℂ × S), x = s.fp q → q ∈ interior u
io : IsOpen i
ia : (c, a) ∈ i
⊢ ∃ t, Barrier s c n t