internlm/Lean-Github huggingface dataset:
Theorem: Super.ray_surj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
⊢ False
Tactic:
have io : IsOpen i := by
  rw [isOpen_iff_eventually]; intro z ⟨x, m, xz⟩
  have eq := (s.ray_nontrivial m).nhds_eq_map_nhds; rw [xz] at eq
  rw [eq, Filter.eventually_map]
  exact ((s.isOpen_ext.snd_preimage c).eventually_mem m).mp
    (eventually_of_forall fun x m ↦ ⟨x, m, rfl⟩)
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
⊢ False
Theorem: Super.ray_surj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
⊢ False
Tactic:
have uc : IsCompact u := ((isClosed_le pc continuous_const).sdiff io).isCompact
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
⊢ False
Theorem: Super.ray_surj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
⊢ False
Tactic:
have z0u : z0 ∈ u := by
  simp only [mem_diff, mem_setOf, u]; use p01.le; contrapose i0
  simp only [not_not, mem_image, mem_setOf, not_forall, exists_prop] at i0 ⊢; exact i0
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
⊢ False
Theorem: Super.ray_surj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
⊢ False
Tactic:
have ne : u.Nonempty := ⟨z0, z0u⟩
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
⊢ False
Theorem: Super.ray_surj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
⊢ False
Tactic:
rcases uc.exists_isMinOn ne pc.continuousOn with ⟨z, zu, zm⟩
Proof state after:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zu : z ∈ u
zm : IsMinOn (s.potential c) u z
⊢ False
Theorem: Super.ray_surj
Proof state before:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zu : z ∈ u
zm : IsMinOn (s.potential c) u z
⊢ False
Tactic:
simp only [mem_diff, mem_setOf, u] at zu
Proof state after:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : IsMinOn (s.potential c) u z
zu : s.potential c z ≤ p1 ∧ z ∉ i
⊢ False
Theorem: Super.ray_surj
Proof state before:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zu : s.potential c z ≤ p1 ∧ z ∉ i
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
⊢ False
Tactic:
simp only [mem_setOf, mem_image, not_exists, not_and, i] at zu
Proof state after:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
⊢ False
Theorem: Super.ray_surj
Proof state before:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
⊢ False
Tactic:
have za := s.potential_minima_only_a (lt_of_le_of_lt zu.1 post) zm
Proof state after:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
za : z = a
⊢ False
Theorem: Super.ray_surj
Proof state before:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
za : z = a
⊢ False
Tactic:
have h := zu.2 0 (s.mem_ext c)
Proof state after:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
za : z = a
h : ¬s.ray c 0 = z
⊢ False
Theorem: Super.ray_surj
Proof state before:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
za : z = a
h : ¬s.ray c 0 = z
⊢ False
Tactic:
simp only [s.ray_zero] at h
Proof state after:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
za : z = a
h : ¬a = z
⊢ False
Theorem: Super.ray_surj
Proof state before:
case 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 x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
io : IsOpen i
jc : IsClosed j
uc : IsCompact u
z0u : z0 ∈ u
ne : u.Nonempty
z : S
zm : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
zu : s.potential c z ≤ p1 ∧ ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z
za : z = a
h : ¬a = z
⊢ False
Tactic:
exact h za.symm
Proof state after:
no goals
Theorem: Super.ray_surj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
⊢ IsOpen i
Tactic:
rw [isOpen_iff_eventually]
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
⊢ ∀ x ∈ i, ∀ᶠ (y : S) in 𝓝 x, y ∈ i
Theorem: Super.ray_surj
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
⊢ ∀ x ∈ i, ∀ᶠ (y : S) in 𝓝 x, y ∈ i
Tactic:
intro z ⟨x, m, xz⟩
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 x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
z : S
x : ℂ
m : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ i
Theorem: Super.ray_surj
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 x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
z : S
x : ℂ
m : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ i
Tactic:
have eq := (s.ray_nontrivial m).nhds_eq_map_nhds
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 x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
z : S
x : ℂ
m : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
eq : 𝓝 (s.ray c x) = Filter.map (s.ray c) (𝓝 x)
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ i
Theorem: Super.ray_surj
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 x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
z : S
x : ℂ
m : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
eq : 𝓝 (s.ray c x) = Filter.map (s.ray c) (𝓝 x)
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ i
Tactic:
rw [xz] at eq
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 x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
z : S
x : ℂ
m : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
eq : 𝓝 z = Filter.map (s.ray c) (𝓝 x)
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ i
Theorem: Super.ray_surj
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 x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
z : S
x : ℂ
m : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
eq : 𝓝 z = Filter.map (s.ray c) (𝓝 x)
⊢ ∀ᶠ (y : S) in 𝓝 z, y ∈ i
Tactic:
rw [eq, Filter.eventually_map]
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 x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
z0 : S
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
m0 : s.potential c z0 < s.p c
p1 : ℝ
p01 : s.potential c z0 < p1
post : p1 < s.p c
i : Set S := s.ray c '' {x | (c, x) ∈ s.ext}
j : Set S := {z | s.potential c z ≤ p1} ∩ i
u : Set S := {z | s.potential c z ≤ p1} \ i
pc : Continuous (s.potential c)
z : S
x : ℂ
m : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
eq : 𝓝 z = Filter.map (s.ray c) (𝓝 x)
⊢ ∀ᶠ (a_1 : ℂ) in 𝓝 x, s.ray c a_1 ∈ i