Theorem: Super.ray_inj
Proof state before:
case holo
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
⊢ HolomorphicAt (I.prod I) I (uncurry fun e x => s.ray e (x1 / x0 * x)) (c, ↑t * x0)

case mem
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
⊢ (c, (f c)^[n] (s.ray c (x1 / x0 * (↑t * x0)))) ∈ s.near

case loc
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), s.bottcherNear y.1 ((f y.1)^[n] (s.ray y.1 (x1 / x0 * y.2))) = y.2 ^ d ^ n
Tactic:
exact (s.ray_holomorphic (pt p1 m)).comp₂_of_eq holomorphicAt_fst
    (holomorphicAt_const.mul holomorphicAt_snd) (by simp only [xe])
Proof state after:
case mem
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
⊢ (c, (f c)^[n] (s.ray c (x1 / x0 * (↑t * x0)))) ∈ s.near

case loc
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), s.bottcherNear y.1 ((f y.1)^[n] (s.ray y.1 (x1 / x0 * y.2))) = y.2 ^ d ^ n