internlm/Lean-Github huggingface dataset:
Theorem: Super.ray_inj
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
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
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)}
h : Ioc 0 1 ⊆ u
tc : Tendsto (fun x => (↑x * x0, ↑x * x1)) (𝓝 0) (𝓝 (0, 0))
inj✝ :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    s.ray c (↑x * x0, ↑x * x1).1 = s.ray c (↑x * x0, ↑x * x1).2 → (↑x * x0, ↑x * x1).1 = (↑x * x0, ↑x * x1).2
r : ℝ
rp : r > 0
inj : ∀ ⦃y : ℝ⦄, |y| < r → s.ray c (↑y * x0) = s.ray c (↑y * x1) → ↑y * x0 = ↑y * x1
t : ℝ := min 1 (r / 2)
t0 : 0 < t
t01 : t ∈ Ioc 0 1
⊢ x0 = x1
Tactic:
specialize @inj t (by simp only [abs_of_pos t0, min_lt_of_right_lt (half_lt_self rp)]) (h t01)
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
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
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)}
h : Ioc 0 1 ⊆ u
tc : Tendsto (fun x => (↑x * x0, ↑x * x1)) (𝓝 0) (𝓝 (0, 0))
inj✝ :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    s.ray c (↑x * x0, ↑x * x1).1 = s.ray c (↑x * x0, ↑x * x1).2 → (↑x * x0, ↑x * x1).1 = (↑x * x0, ↑x * x1).2
r : ℝ
rp : r > 0
t : ℝ := min 1 (r / 2)
t0 : 0 < t
t01 : t ∈ Ioc 0 1
inj : ↑t * x0 = ↑t * x1
⊢ x0 = x1
Theorem: Super.ray_inj
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
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
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)}
h : Ioc 0 1 ⊆ u
tc : Tendsto (fun x => (↑x * x0, ↑x * x1)) (𝓝 0) (𝓝 (0, 0))
inj✝ :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    s.ray c (↑x * x0, ↑x * x1).1 = s.ray c (↑x * x0, ↑x * x1).2 → (↑x * x0, ↑x * x1).1 = (↑x * x0, ↑x * x1).2
r : ℝ
rp : r > 0
t : ℝ := min 1 (r / 2)
t0 : 0 < t
t01 : t ∈ Ioc 0 1
inj : ↑t * x0 = ↑t * x1
⊢ x0 = x1
Tactic:
exact mul_left_cancel₀ (Complex.ofReal_ne_zero.mpr t0.ne') inj
Proof state after:
no goals
Theorem: Super.ray_inj
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
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
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)}
h : Ioc 0 1 ⊆ u
tc : Tendsto (fun x => (↑x * x0, ↑x * x1)) (𝓝 0) (𝓝 (0, 0))
inj✝ :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    s.ray c (↑x * x0, ↑x * x1).1 = s.ray c (↑x * x0, ↑x * x1).2 → (↑x * x0, ↑x * x1).1 = (↑x * x0, ↑x * x1).2
r : ℝ
rp : r > 0
inj : ∀ ⦃y : ℝ⦄, |y| < r → s.ray c (↑y * x0) = s.ray c (↑y * x1) → ↑y * x0 = ↑y * x1
t : ℝ := min 1 (r / 2)
t0 : 0 < t
t01 : t ∈ Ioc 0 1
⊢ |t| < r
Tactic:
simp only [abs_of_pos t0, min_lt_of_right_lt (half_lt_self rp)]
Proof state after:
no goals
Theorem: Super.ray_inj
Proof state before:
case neg.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)}
⊢ (Ioc 0 1 ∩ u).Nonempty
Tactic:
use 1, right_mem_Ioc.mpr zero_lt_one
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
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)}
⊢ 1 ∈ u
Theorem: Super.ray_inj
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
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)}
⊢ 1 ∈ u
Tactic:
simp only [mem_setOf, Complex.ofReal_one, one_mul, e, u]
Proof state after:
no goals
Theorem: Super.ray_inj
Proof state before:
case neg.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)}
⊢ Ioc 0 1 ∩ u ⊆ interior u
Tactic:
intro t ⟨m, e⟩
Proof state after:
case neg.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
⊢ t ∈ interior u
Theorem: Super.ray_inj
Proof state before:
case neg.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
⊢ t ∈ interior u
Tactic:
simp only [mem_setOf, mem_interior_iff_mem_nhds, ← Filter.eventually_iff] at e ⊢
Proof state after:
case neg.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
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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
⊢ u ∈ 𝓝 t
Tactic:
generalize hn : s.np c (abs (↑t * x0)) = n
Proof state after:
case neg.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
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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
⊢ u ∈ 𝓝 t
Tactic:
have t0 : (t : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr m.1.ne'
Proof state after:
case neg.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
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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
⊢ u ∈ 𝓝 t
Tactic:
have pe : abs (↑t * x0) = abs (↑t * x1) := by
  simp only [mem_setOf_eq, u] at e
  simp only [← s.ray_potential (pt p0 m), e, ← s.ray_potential (pt p1 m)]
Proof state after:
case neg.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)
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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)
⊢ u ∈ 𝓝 t
Tactic:
have e0 := (s.ray_spec (Complex.abs.nonneg _) (pt p0 m)).eqn.filter_mono
  (nhds_le_nhdsSet mem_domain_self)
Proof state after:
case neg.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).1, (c, ↑t * x0).2), Eqn s (s.np (c, ↑t * x0).1 (Complex.abs (c, ↑t * x0).2)) s.ray x
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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).1, (c, ↑t * x0).2), Eqn s (s.np (c, ↑t * x0).1 (Complex.abs (c, ↑t * x0).2)) s.ray x
⊢ u ∈ 𝓝 t
Tactic:
have e1 := (s.ray_spec (Complex.abs.nonneg _) (pt p1 m)).eqn.filter_mono
  (nhds_le_nhdsSet mem_domain_self)
Proof state after:
case neg.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).1, (c, ↑t * x0).2), Eqn s (s.np (c, ↑t * x0).1 (Complex.abs (c, ↑t * x0).2)) s.ray x
e1 :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 ((c, ↑t * x1).1, (c, ↑t * x1).2), Eqn s (s.np (c, ↑t * x1).1 (Complex.abs (c, ↑t * x1).2)) s.ray x
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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).1, (c, ↑t * x0).2), Eqn s (s.np (c, ↑t * x0).1 (Complex.abs (c, ↑t * x0).2)) s.ray x
e1 :
  ∀ᶠ (x : ℂ × ℂ) in 𝓝 ((c, ↑t * x1).1, (c, ↑t * x1).2), Eqn s (s.np (c, ↑t * x1).1 (Complex.abs (c, ↑t * x1).2)) s.ray x
⊢ u ∈ 𝓝 t
Tactic:
simp only [← pe, hn] at e0 e1
Proof state after:
case neg.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
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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
⊢ u ∈ 𝓝 t
Tactic:
have de : (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n := by
  have e0 := e0.self_of_nhds.eqn
  have e1 := e1.self_of_nhds.eqn
  simp only [mem_setOf_eq, u] at e
  simp only [hn, ← pe, ← e] at e0 e1
  exact e0.symm.trans e1
Proof state after:
case neg.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 : (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
⊢ u ∈ 𝓝 t
Theorem: Super.ray_inj
Proof state before:
case neg.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 : (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
⊢ u ∈ 𝓝 t
Tactic:
simp only [mul_pow] at de
Proof state after:
case neg.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 : ↑t ^ d ^ n * x0 ^ d ^ n = ↑t ^ d ^ n * x1 ^ d ^ n
⊢ u ∈ 𝓝 t