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
er : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, ↑t * x0), Eqn s n r y
⊢ u ∈ 𝓝 t
Tactic:
refine ((continuousAt_const.prod (Complex.continuous_ofReal.continuousAt.mul
    continuousAt_const)).eventually
    (eqn_unique e0 er ?_ (mul_ne_zero t0 x00))).mp (eventually_of_forall fun u e ↦ ?_)
Proof state after:
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 ((fun x => (c, ↑x * x0)) t).1 ((fun x => (c, ↑x * x0)) t).2 =
    r ((fun x => (c, ↑x * x0)) t).1 ((fun x => (c, ↑x * x0)) t).2

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)