internlm/Lean-Github huggingface dataset:
Theorem: Super.ray_inj
Proof state before:
case neg.refine_2.refine_1
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e : t ∈ u
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
⊢ s.ray c (↑t * x0) = s.ray c (↑t * x1)
Tactic:
exact e
Proof state after:
no goals
Theorem: Super.ray_inj
Proof state before:
case neg.refine_2.refine_2
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝¹ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u✝ : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e✝ : t ∈ u✝
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
u : ℝ
e : uncurry s.ray (c, ↑u * x0) = uncurry r (c, ↑u * x0)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Tactic:
rw [← hr] at e
Proof state after:
case neg.refine_2.refine_2
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝¹ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u✝ : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e✝ : t ∈ u✝
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
u : ℝ
e : uncurry s.ray (c, ↑u * x0) = uncurry (fun e x => s.ray e (x1 / x0 * x)) (c, ↑u * x0)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Theorem: Super.ray_inj
Proof state before:
case neg.refine_2.refine_2
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝¹ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u✝ : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e✝ : t ∈ u✝
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
u : ℝ
e : uncurry s.ray (c, ↑u * x0) = uncurry (fun e x => s.ray e (x1 / x0 * x)) (c, ↑u * x0)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Tactic:
simp only [uncurry] at e
Proof state after:
case neg.refine_2.refine_2
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝¹ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u✝ : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e✝ : t ∈ u✝
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
u : ℝ
e : s.ray c (↑u * x0) = s.ray c (x1 / x0 * (↑u * x0))
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Theorem: Super.ray_inj
Proof state before:
case neg.refine_2.refine_2
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝¹ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u✝ : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e✝ : t ∈ u✝
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
u : ℝ
e : s.ray c (↑u * x0) = s.ray c (x1 / x0 * (↑u * x0))
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Tactic:
rw [← mul_assoc, mul_comm _ (u:ℂ), mul_assoc, div_mul_cancel₀ _ x00] at e
Proof state after:
case neg.refine_2.refine_2
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝¹ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u✝ : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e✝ : t ∈ u✝
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
u : ℝ
e : s.ray c (↑u * x0) = s.ray c (↑u * x1)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Theorem: Super.ray_inj
Proof state before:
case neg.refine_2.refine_2
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝¹ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u✝ : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e✝ : t ∈ u✝
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
pe : Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
e0 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n s.ray x
e1 : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, ↑t * x1), Eqn s n s.ray x
de : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
xe : x1 / x0 * (↑t * x0) = ↑t * x1
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
u : ℝ
e : s.ray c (↑u * x0) = s.ray c (↑u * x1)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Tactic:
exact e
Proof state after:
no goals
Theorem: Super.ray_inj
Proof state before:
case neg.refine_3
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
⊢ Ioc 0 1 ∩ closure u ⊆ u
Tactic:
intro t ⟨m, e⟩
Proof state after:
case neg.refine_3
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e : t ∈ closure u
⊢ t ∈ u
Theorem: Super.ray_inj
Proof state before:
case neg.refine_3
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e : t ∈ closure u
⊢ t ∈ u
Tactic:
simp only [mem_setOf, mem_closure_iff_frequently] at e ⊢
Proof state after:
case neg.refine_3
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
⊢ t ∈ u
Theorem: Super.ray_inj
Proof state before:
case neg.refine_3
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
⊢ t ∈ u
Tactic:
have rc : ∀ {x : ℂ}, (c, x) ∈ s.ext → ContinuousAt (fun t : ℝ ↦ s.ray c (↑t * x)) t :=
  fun {x} p ↦
  (s.ray_holomorphic (pt p m)).along_snd.continuousAt.comp_of_eq
    (Complex.continuous_ofReal.continuousAt.mul continuousAt_const) rfl
Proof state after:
case neg.refine_3
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
rc : ∀ {x : ℂ}, (c, x) ∈ s.ext → ContinuousAt (fun t => s.ray c (↑t * x)) t
⊢ t ∈ u
Theorem: Super.ray_inj
Proof state before:
case neg.refine_3
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
x0 x1 : ℂ
p0 : (c, x0) ∈ s.ext
p1 : (c, x1) ∈ s.ext
e✝ : s.ray c x0 = s.ray c x1
ax : Complex.abs x0 = Complex.abs x1
x00 : ¬x0 = 0
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
u : Set ℝ := {t | s.ray c (↑t * x0) = s.ray c (↑t * x1)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
rc : ∀ {x : ℂ}, (c, x) ∈ s.ext → ContinuousAt (fun t => s.ray c (↑t * x)) t
⊢ t ∈ u
Tactic:
exact tendsto_nhds_unique_of_frequently_eq (rc p0) (rc p1) e
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
⊢ ∀ {z : S}, (c, z) ∈ s.post → ∃ x, (c, x) ∈ s.ext ∧ s.ray c x = z
Tactic:
intro z0 m0
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
m0 : (c, z0) ∈ s.post
⊢ ∃ x, (c, x) ∈ s.ext ∧ s.ray c x = z0
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
m0 : (c, z0) ∈ s.post
⊢ ∃ x, (c, x) ∈ s.ext ∧ s.ray c x = z0
Tactic:
by_contra i0
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
m0 : (c, z0) ∈ s.post
i0 : ¬∃ x, (c, x) ∈ s.ext ∧ s.ray c x = z0
⊢ False
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
m0 : (c, z0) ∈ s.post
i0 : ¬∃ x, (c, x) ∈ s.ext ∧ s.ray c x = z0
⊢ False
Tactic:
simp only [not_forall, not_exists, not_and] at i0
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
m0 : (c, z0) ∈ s.post
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
⊢ False
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
m0 : (c, z0) ∈ s.post
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
⊢ False
Tactic:
set p0 := s.potential c z0
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
m0 : (c, z0) ∈ s.post
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
⊢ False
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
m0 : (c, z0) ∈ s.post
i0 : ∀ (x : ℂ), (c, x) ∈ s.ext → ¬s.ray c x = z0
p0 : ℝ := s.potential c z0
⊢ False
Tactic:
simp only [Super.post, mem_setOf, Postcritical] at m0
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
⊢ False
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
⊢ False
Tactic:
rcases exists_between m0 with ⟨p1, p01, post⟩
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
⊢ 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
⊢ False
Tactic:
set i := s.ray c '' {x | (c, x) ∈ s.ext}
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}
⊢ 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}
⊢ False
Tactic:
set j := {z | s.potential c z ≤ p1} ∩ i
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
⊢ 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
⊢ False
Tactic:
set u := {z | s.potential c z ≤ p1} \ i
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
⊢ 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
⊢ False
Tactic:
have pc : Continuous (s.potential c) := (Continuous.potential s).along_snd
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)
⊢ False