internlm/Lean-Github huggingface dataset:
Theorem: Super.ray_surj
Proof state before:
case right
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
⊢ z0 ∉ i
Tactic:
contrapose i0
Proof state after:
case right
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
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
i0 : ¬z0 ∉ i
⊢ ¬∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
Theorem: Super.ray_surj
Proof state before:
case right
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
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
i0 : ¬z0 ∉ i
⊢ ¬∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
Tactic:
simp only [not_not, mem_image, mem_setOf, not_forall, exists_prop] at i0 ⊢
Proof state after:
case right
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
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
i0 : z0 ∈ i
⊢ ∃ x, (c, x) ∈ s.ext ∧ s.ray c x = z0
Theorem: Super.ray_surj
Proof state before:
case right
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
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
i0 : z0 ∈ i
⊢ ∃ x, (c, x) ∈ s.ext ∧ s.ray c x = z0
Tactic:
exact i0
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)
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
⊢ ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
Tactic:
have m : z ∈ jᶜ := by rw [compl_inter]; right; exact zu.2
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)
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
m : z ∈ jᶜ
⊢ ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
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)
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
m : z ∈ jᶜ
⊢ ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
Tactic:
have lt : s.potential c z < p1 := lt_of_le_of_lt (zm z0u) p01
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)
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
m : z ∈ jᶜ
lt : s.potential c z < p1
⊢ ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
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)
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
m : z ∈ jᶜ
lt : s.potential c z < p1
⊢ ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
Tactic:
apply (jc.isOpen_compl.eventually_mem m).mp
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)
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
m : z ∈ jᶜ
lt : s.potential c z < p1
⊢ ∀ᶠ (x : S) in 𝓝 z, x ∈ jᶜ → s.potential c z ≤ s.potential c x
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)
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
m : z ∈ jᶜ
lt : s.potential c z < p1
⊢ ∀ᶠ (x : S) in 𝓝 z, x ∈ jᶜ → s.potential c z ≤ s.potential c x
Tactic:
apply ((Continuous.potential s).along_snd.continuousAt.eventually_lt continuousAt_const lt).mp
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)
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
m : z ∈ jᶜ
lt : s.potential c z < p1
⊢ ∀ᶠ (x : S) in 𝓝 z, uncurry s.potential (c, x) < p1 → x ∈ jᶜ → s.potential c z ≤ s.potential c x
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)
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
m : z ∈ jᶜ
lt : s.potential c z < p1
⊢ ∀ᶠ (x : S) in 𝓝 z, uncurry s.potential (c, x) < p1 → x ∈ jᶜ → s.potential c z ≤ s.potential c x
Tactic:
refine eventually_of_forall fun w lt m ↦ ?_
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)
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ jᶜ
⊢ s.potential c z ≤ s.potential c w
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)
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ jᶜ
⊢ s.potential c z ≤ s.potential c w
Tactic:
rw [compl_inter] at m
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)
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ {z | s.potential c z ≤ p1}ᶜ ∪ iᶜ
⊢ s.potential c z ≤ s.potential c w
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)
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ {z | s.potential c z ≤ p1}ᶜ ∪ iᶜ
⊢ s.potential c z ≤ s.potential c w
Tactic:
cases' m with m m
Proof state after:
case inl
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ {z | s.potential c z ≤ p1}ᶜ
⊢ s.potential c z ≤ s.potential c w

case inr
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ iᶜ
⊢ s.potential c z ≤ s.potential c w
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)
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
⊢ z ∈ jᶜ
Tactic:
rw [compl_inter]
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)
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
⊢ z ∈ {z | s.potential c z ≤ p1}ᶜ ∪ 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)
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
⊢ z ∈ {z | s.potential c z ≤ p1}ᶜ ∪ iᶜ
Tactic:
right
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 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
⊢ z ∈ iᶜ
Theorem: Super.ray_surj
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 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
⊢ z ∈ iᶜ
Tactic:
exact zu.2
Proof state after:
no goals
Theorem: Super.ray_surj
Proof state before:
case inl
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : w ∈ {z | s.potential c z ≤ p1}ᶜ
⊢ s.potential c z ≤ s.potential c w
Tactic:
simp only [compl_setOf, mem_setOf, not_le] at m
Proof state after:
case inl
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : p1 < s.potential c w
⊢ s.potential c z ≤ s.potential c w
Theorem: Super.ray_surj
Proof state before:
case inl
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
m✝ : z ∈ jᶜ
lt✝ : s.potential c z < p1
w : S
lt : uncurry s.potential (c, w) < p1
m : p1 < s.potential c w
⊢ s.potential c z ≤ s.potential c w
Tactic:
linarith
Proof state after:
no goals