internlm/Lean-Github huggingface dataset:
Theorem: Super.ray_inj
Proof state before:
case neg
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 ⊆ interior u
Tactic:
refine isPreconnected_Ioc.relative_clopen ?_ ?_ ?_
Proof state after:
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

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

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
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
⊢ Complex.abs x0 = Complex.abs x1
Tactic:
simp only [← s.ray_potential p0, ← s.ray_potential p1, e]
Proof state after:
no goals
Theorem: Super.ray_inj
Proof state before:
case pos
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
⊢ x0 = x1
Tactic:
simp only [x00, Complex.abs.map_zero] at ax ⊢
Proof state after:
case pos
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
x00 : x0 = 0
ax : 0 = Complex.abs x1
⊢ 0 = x1
Theorem: Super.ray_inj
Proof state before:
case pos
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
x00 : x0 = 0
ax : 0 = Complex.abs x1
⊢ 0 = x1
Tactic:
exact (Complex.abs.eq_zero.mp ax.symm).symm
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
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
⊢ ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc 0 1 → (c, ↑t * x) ∈ s.ext
Tactic:
intro x t p 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
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
x : ℂ
t : ℝ
p : (c, x) ∈ s.ext
m : t ∈ Ioc 0 1
⊢ (c, ↑t * x) ∈ s.ext
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
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
x : ℂ
t : ℝ
p : (c, x) ∈ s.ext
m : t ∈ Ioc 0 1
⊢ (c, ↑t * x) ∈ s.ext
Tactic:
simp only [Super.ext, mem_setOf, Complex.abs.map_mul, Complex.abs_ofReal, abs_of_pos m.1] at p ⊢
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
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
x : ℂ
t : ℝ
m : t ∈ Ioc 0 1
p : Complex.abs x < s.p c
⊢ t * Complex.abs x < s.p c
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
tc : ∀ (x : ℂ) (t : ℝ), ContinuousAt (fun t => ↑t * x) t
x : ℂ
t : ℝ
m : t ∈ Ioc 0 1
p : Complex.abs x < s.p c
⊢ t * Complex.abs x < s.p c
Tactic:
exact lt_of_le_of_lt (mul_le_of_le_one_left (Complex.abs.nonneg _) m.2) p
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
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)}
h : Ioc 0 1 ⊆ interior u
⊢ x0 = x1
Tactic:
replace h := _root_.trans h interior_subset
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
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)}
h : Ioc 0 1 ⊆ u
⊢ x0 = x1
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
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)}
h : Ioc 0 1 ⊆ u
⊢ x0 = x1
Tactic:
replace tc := (tc x0 0).prod_mk (tc x1 0)
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
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) (𝓝 ((fun t => ↑t * x0) 0) ×ˢ 𝓝 ((fun t => ↑t * x1) 0))
⊢ x0 = x1
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) (𝓝 ((fun t => ↑t * x0) 0) ×ˢ 𝓝 ((fun t => ↑t * x1) 0))
⊢ x0 = x1
Tactic:
simp only [← nhds_prod_eq] at tc
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
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 * x0, ↑0 * x1))
⊢ x0 = x1
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 * x0, ↑0 * x1))
⊢ x0 = x1
Tactic:
simp only [ContinuousAt, Complex.ofReal_zero, MulZeroClass.zero_mul] at tc
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
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))
⊢ x0 = x1
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))
⊢ x0 = x1
Tactic:
have inj := tc.eventually ((s.ray_holomorphic (s.mem_ext c)).along_snd.local_inj
  (s.ray_noncritical_zero c))
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
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
⊢ x0 = x1
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
⊢ x0 = x1
Tactic:
rcases Metric.eventually_nhds_iff.mp inj with ⟨r, rp, inj⟩
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
inj :
  ∀ ⦃y : ℝ⦄,
    dist y 0 < r →
      s.ray c (↑y * x0, ↑y * x1).1 = s.ray c (↑y * x0, ↑y * x1).2 → (↑y * x0, ↑y * x1).1 = (↑y * x0, ↑y * x1).2
⊢ 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
inj :
  ∀ ⦃y : ℝ⦄,
    dist y 0 < r →
      s.ray c (↑y * x0, ↑y * x1).1 = s.ray c (↑y * x0, ↑y * x1).2 → (↑y * x0, ↑y * x1).1 = (↑y * x0, ↑y * x1).2
⊢ x0 = x1
Tactic:
simp only [Real.dist_eq, sub_zero] at inj
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
inj : ∀ ⦃y : ℝ⦄, |y| < r → s.ray c (↑y * x0) = s.ray c (↑y * x1) → ↑y * x0 = ↑y * 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
inj : ∀ ⦃y : ℝ⦄, |y| < r → s.ray c (↑y * x0) = s.ray c (↑y * x1) → ↑y * x0 = ↑y * x1
⊢ x0 = x1
Tactic:
set t := min 1 (r / 2)
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
inj : ∀ ⦃y : ℝ⦄, |y| < r → s.ray c (↑y * x0) = s.ray c (↑y * x1) → ↑y * x0 = ↑y * x1
t : ℝ := min 1 (r / 2)
⊢ 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
inj : ∀ ⦃y : ℝ⦄, |y| < r → s.ray c (↑y * x0) = s.ray c (↑y * x1) → ↑y * x0 = ↑y * x1
t : ℝ := min 1 (r / 2)
⊢ x0 = x1
Tactic:
have t0 : 0 < t := lt_min zero_lt_one (half_pos rp)
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
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
⊢ 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
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
⊢ x0 = x1
Tactic:
have t01 : t ∈ Ioc (0 : ℝ) 1 := mem_Ioc.mpr ⟨t0, min_le_left _ _⟩
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
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