internlm/Lean-Github huggingface dataset:
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)
⊢ ∀ᶠ (a_1 : ℂ) in 𝓝 x, s.ray c a_1 ∈ i
Tactic:
exact ((s.isOpen_ext.snd_preimage c).eventually_mem m).mp
  (eventually_of_forall fun x m ↦ ⟨x, m, rfl⟩)
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
e : j = s.ray c '' closedBall 0 p1
⊢ IsClosed j
Tactic:
rw [e]
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
e : j = s.ray c '' closedBall 0 p1
⊢ IsClosed (s.ray c '' closedBall 0 p1)
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
e : j = s.ray c '' closedBall 0 p1
⊢ IsClosed (s.ray c '' closedBall 0 p1)
Tactic:
refine (IsCompact.image_of_continuousOn (isCompact_closedBall _ _) ?_).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 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
e : j = s.ray c '' closedBall 0 p1
⊢ ContinuousOn (s.ray c) (closedBall 0 p1)
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
e : j = s.ray c '' closedBall 0 p1
⊢ ContinuousOn (s.ray c) (closedBall 0 p1)
Tactic:
intro x 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
e : j = s.ray c '' closedBall 0 p1
x : ℂ
m : x ∈ closedBall 0 p1
⊢ ContinuousWithinAt (s.ray c) (closedBall 0 p1) 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
e : j = s.ray c '' closedBall 0 p1
x : ℂ
m : x ∈ closedBall 0 p1
⊢ ContinuousWithinAt (s.ray c) (closedBall 0 p1) x
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero] 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
e : j = s.ray c '' closedBall 0 p1
x : ℂ
m : Complex.abs x ≤ p1
⊢ ContinuousWithinAt (s.ray c) (closedBall 0 p1) 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
e : j = s.ray c '' closedBall 0 p1
x : ℂ
m : Complex.abs x ≤ p1
⊢ ContinuousWithinAt (s.ray c) (closedBall 0 p1) x
Tactic:
exact (s.ray_holomorphic (lt_of_le_of_lt m post)).along_snd.continuousAt.continuousWithinAt
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
⊢ j = s.ray c '' closedBall 0 p1
Tactic:
refine Set.ext fun z ↦ ?_
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
z : S
⊢ z ∈ j ↔ z ∈ s.ray c '' closedBall 0 p1
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
z : S
⊢ z ∈ j ↔ z ∈ s.ray c '' closedBall 0 p1
Tactic:
simp only [mem_inter_iff, mem_setOf, mem_image, mem_closedBall, Complex.dist_eq, sub_zero,
  Super.ext, j]
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
z : S
⊢ s.potential c z ≤ p1 ∧ z ∈ i ↔ ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z
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
z : S
⊢ s.potential c z ≤ p1 ∧ z ∈ i ↔ ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z
Tactic:
constructor
Proof state after:
case mp
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
z : S
⊢ s.potential c z ≤ p1 ∧ z ∈ i → ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z

case mpr
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
z : S
⊢ (∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z) → s.potential c z ≤ p1 ∧ z ∈ i
Theorem: Super.ray_surj
Proof state before:
case mp
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
z : S
⊢ s.potential c z ≤ p1 ∧ z ∈ i → ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z
Tactic:
intro ⟨zp1, x, xp, xz⟩
Proof state after:
case mp
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
z : S
zp1 : s.potential c z ≤ p1
x : ℂ
xp : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
⊢ ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z
Theorem: Super.ray_surj
Proof state before:
case mp
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
z : S
zp1 : s.potential c z ≤ p1
x : ℂ
xp : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
⊢ ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z
Tactic:
rw [← xz, s.ray_potential xp] at zp1
Proof state after:
case mp
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
z : S
x : ℂ
zp1 : Complex.abs x ≤ p1
xp : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
⊢ ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z
Theorem: Super.ray_surj
Proof state before:
case mp
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
z : S
x : ℂ
zp1 : Complex.abs x ≤ p1
xp : x ∈ {x | (c, x) ∈ s.ext}
xz : s.ray c x = z
⊢ ∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z
Tactic:
use x, zp1, xz
Proof state after:
no goals
Theorem: Super.ray_surj
Proof state before:
case mpr
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
z : S
⊢ (∃ x, Complex.abs x ≤ p1 ∧ s.ray c x = z) → s.potential c z ≤ p1 ∧ z ∈ i
Tactic:
intro ⟨x, xp, xz⟩
Proof state after:
case mpr
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
z : S
x : ℂ
xp : Complex.abs x ≤ p1
xz : s.ray c x = z
⊢ s.potential c z ≤ p1 ∧ z ∈ i
Theorem: Super.ray_surj
Proof state before:
case mpr
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
z : S
x : ℂ
xp : Complex.abs x ≤ p1
xz : s.ray c x = z
⊢ s.potential c z ≤ p1 ∧ z ∈ i
Tactic:
have zp1 := lt_of_le_of_lt xp post
Proof state after:
case mpr
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
z : S
x : ℂ
xp : Complex.abs x ≤ p1
xz : s.ray c x = z
zp1 : Complex.abs x < s.p c
⊢ s.potential c z ≤ p1 ∧ z ∈ i
Theorem: Super.ray_surj
Proof state before:
case mpr
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
z : S
x : ℂ
xp : Complex.abs x ≤ p1
xz : s.ray c x = z
zp1 : Complex.abs x < s.p c
⊢ s.potential c z ≤ p1 ∧ z ∈ i
Tactic:
rw [← xz, s.ray_potential zp1]
Proof state after:
case mpr
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
z : S
x : ℂ
xp : Complex.abs x ≤ p1
xz : s.ray c x = z
zp1 : Complex.abs x < s.p c
⊢ Complex.abs x ≤ p1 ∧ s.ray c x ∈ i
Theorem: Super.ray_surj
Proof state before:
case mpr
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
z : S
x : ℂ
xp : Complex.abs x ≤ p1
xz : s.ray c x = z
zp1 : Complex.abs x < s.p c
⊢ Complex.abs x ≤ p1 ∧ s.ray c x ∈ i
Tactic:
use xp, x, zp1
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
⊢ z0 ∈ u
Tactic:
simp only [mem_diff, mem_setOf, u]
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
⊢ s.potential c z0 ≤ p1 ∧ z0 ∉ 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
⊢ s.potential c z0 ≤ p1 ∧ z0 ∉ i
Tactic:
use p01.le
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
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