internlm/Lean-Github huggingface dataset:
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 ^ d ^ n * x0 ^ d ^ n = ↑t ^ d ^ n * x1 ^ d ^ n
⊢ u ∈ 𝓝 t
Tactic:
replace de := mul_left_cancel₀ (pow_ne_zero _ t0) 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 : x0 ^ d ^ n = 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 : x0 ^ d ^ n = x1 ^ d ^ n
⊢ u ∈ 𝓝 t
Tactic:
generalize hr : (fun e x ↦ s.ray e (x1 / x0 * x)) = r
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 : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
⊢ 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 : x0 ^ d ^ n = x1 ^ d ^ n
r : ℂ → ℂ → S
hr : (fun e x => s.ray e (x1 / x0 * x)) = r
⊢ u ∈ 𝓝 t
Tactic:
have xe : x1 / x0 * (↑t * x0) = ↑t * x1 := by
  rw [← mul_assoc, mul_comm _ (t:ℂ), mul_assoc, div_mul_cancel₀ _ x00]
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 : 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
⊢ 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 : 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
⊢ u ∈ 𝓝 t
Tactic:
have er : ∀ᶠ y in 𝓝 (c, ↑t * x0), Eqn s n r y := by
  rw [← hr]; apply eqn_near
  exact (s.ray_holomorphic (pt p1 m)).comp₂_of_eq holomorphicAt_fst
      (holomorphicAt_const.mul holomorphicAt_snd) (by simp only [xe])
  rw [xe]; exact e1.self_of_nhds.near
  have xc : ContinuousAt (fun y : ℂ × ℂ ↦ (y.1, x1 / x0 * y.2)) (c, ↑t * x0) :=
    continuousAt_fst.prod (continuousAt_const.mul continuousAt_snd)
  simp only [ContinuousAt] at xc
  rw [← mul_assoc, mul_comm _ (t:ℂ), mul_assoc, div_mul_cancel₀ _ x00] at xc
  refine (xc.eventually e1).mp (eventually_of_forall ?_); intro ⟨e, x⟩ e1
  exact _root_.trans e1.eqn (by
    simp only [mul_pow, div_pow, ← de, div_self (pow_ne_zero _ x00), one_mul])
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 : 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 ∈ 𝓝 t
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : t ∈ u
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
⊢ Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
Tactic:
simp only [mem_setOf_eq, u] at 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
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 : s.ray c (↑t * x0) = s.ray c (↑t * x1)
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
⊢ Complex.abs (↑t * x0) = Complex.abs (↑t * 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)}
t : ℝ
m : t ∈ Ioc 0 1
e : s.ray c (↑t * x0) = s.ray c (↑t * x1)
n : ℕ
hn : s.np c (Complex.abs (↑t * x0)) = n
t0 : ↑t ≠ 0
⊢ Complex.abs (↑t * x0) = Complex.abs (↑t * x1)
Tactic:
simp only [← s.ray_potential (pt p0 m), e, ← s.ray_potential (pt p1 m)]
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)}
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
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
Tactic:
have e0 := e0.self_of_nhds.eqn
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)}
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
e0 :
  s.bottcherNear (c, ↑t * x0).1 ((f (c, ↑t * x0).1)^[n] (s.ray (c, ↑t * x0).1 (c, ↑t * x0).2)) = (c, ↑t * x0).2 ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
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)}
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
e0 :
  s.bottcherNear (c, ↑t * x0).1 ((f (c, ↑t * x0).1)^[n] (s.ray (c, ↑t * x0).1 (c, ↑t * x0).2)) = (c, ↑t * x0).2 ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
Tactic:
have e1 := e1.self_of_nhds.eqn
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)}
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
e0 :
  s.bottcherNear (c, ↑t * x0).1 ((f (c, ↑t * x0).1)^[n] (s.ray (c, ↑t * x0).1 (c, ↑t * x0).2)) = (c, ↑t * x0).2 ^ d ^ n
e1 :
  s.bottcherNear (c, ↑t * x1).1 ((f (c, ↑t * x1).1)^[n] (s.ray (c, ↑t * x1).1 (c, ↑t * x1).2)) = (c, ↑t * x1).2 ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
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)}
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
e0 :
  s.bottcherNear (c, ↑t * x0).1 ((f (c, ↑t * x0).1)^[n] (s.ray (c, ↑t * x0).1 (c, ↑t * x0).2)) = (c, ↑t * x0).2 ^ d ^ n
e1 :
  s.bottcherNear (c, ↑t * x1).1 ((f (c, ↑t * x1).1)^[n] (s.ray (c, ↑t * x1).1 (c, ↑t * x1).2)) = (c, ↑t * x1).2 ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
Tactic:
simp only [mem_setOf_eq, u] at 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
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 : s.ray c (↑t * x0) = s.ray c (↑t * x1)
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
e0 :
  s.bottcherNear (c, ↑t * x0).1 ((f (c, ↑t * x0).1)^[n] (s.ray (c, ↑t * x0).1 (c, ↑t * x0).2)) = (c, ↑t * x0).2 ^ d ^ n
e1 :
  s.bottcherNear (c, ↑t * x1).1 ((f (c, ↑t * x1).1)^[n] (s.ray (c, ↑t * x1).1 (c, ↑t * x1).2)) = (c, ↑t * x1).2 ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : s.ray c (↑t * x0) = s.ray c (↑t * x1)
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
e0 :
  s.bottcherNear (c, ↑t * x0).1 ((f (c, ↑t * x0).1)^[n] (s.ray (c, ↑t * x0).1 (c, ↑t * x0).2)) = (c, ↑t * x0).2 ^ d ^ n
e1 :
  s.bottcherNear (c, ↑t * x1).1 ((f (c, ↑t * x1).1)^[n] (s.ray (c, ↑t * x1).1 (c, ↑t * x1).2)) = (c, ↑t * x1).2 ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
Tactic:
simp only [hn, ← pe, ← e] at e0 e1
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : s.ray c (↑t * x0) = s.ray c (↑t * x1)
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
e0 : s.bottcherNear c ((f c)^[n] (s.ray c (↑t * x0))) = (↑t * x0) ^ d ^ n
e1 : s.bottcherNear c ((f c)^[n] (s.ray c (↑t * x0))) = (↑t * x1) ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : s.ray c (↑t * x0) = s.ray c (↑t * x1)
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
e0 : s.bottcherNear c ((f c)^[n] (s.ray c (↑t * x0))) = (↑t * x0) ^ d ^ n
e1 : s.bottcherNear c ((f c)^[n] (s.ray c (↑t * x0))) = (↑t * x1) ^ d ^ n
⊢ (↑t * x0) ^ d ^ n = (↑t * x1) ^ d ^ n
Tactic:
exact e0.symm.trans e1
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)}
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
⊢ x1 / x0 * (↑t * x0) = ↑t * x1
Tactic:
rw [← mul_assoc, mul_comm _ (t:ℂ), mul_assoc, div_mul_cancel₀ _ x00]
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)}
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
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
Tactic:
rw [← hr]
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)}
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
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n (fun e x => s.ray e (x1 / x0 * x)) y