Theorem: Super.ray_inj (Ray/Dynamics/Ray.lean)

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 : ℂ
⊢ (c, x0) ∈ s.ext → (c, x1) ∈ s.ext → s.ray c x0 = s.ray c x1 → x0 = x1
Tactic:
intro p0 p1 e
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
⊢ x0 = x1

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
⊢ x0 = x1
Tactic:
have ax : abs x0 = abs x1 := by simp only [← s.ray_potential p0, ← s.ray_potential p1, e]
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
⊢ x0 = x1

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
⊢ x0 = x1
Tactic:
by_cases x00 : x0 = 0
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
ax : Complex.abs x0 = Complex.abs x1
x00 : x0 = 0
⊢ x0 = x1

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
⊢ x0 = x1

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
⊢ x0 = x1
Tactic:
have tc : ∀ (x : ℂ) (t), ContinuousAt (fun t : ℝ ↦ ↑t * x) t := fun x t ↦
  Complex.continuous_ofReal.continuousAt.mul continuousAt_const
State after:
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
⊢ x0 = x1

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
⊢ x0 = x1
Tactic:
have pt : ∀ {x : ℂ} {t : ℝ}, (c, x) ∈ s.ext → t ∈ Ioc (0 : ℝ) 1 → (c, ↑t * x) ∈ s.ext := by
  intro x t p m
  simp only [Super.ext, mem_setOf, Complex.abs.map_mul, Complex.abs_ofReal, abs_of_pos m.1] at p ⊢
  exact lt_of_le_of_lt (mul_le_of_le_one_left (Complex.abs.nonneg _) m.2) p
State after:
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
⊢ x0 = x1

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
⊢ x0 = x1
Tactic:
set u : Set ℝ := {t : ℝ | s.ray c (t * x0) = s.ray c (t * x1)}
State after:
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)}
⊢ x0 = x1

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)}
⊢ x0 = x1
Tactic:
suffices h : Ioc (0 : ℝ) 1 ⊆ interior u by
  replace h := _root_.trans h interior_subset
  replace tc := (tc x0 0).prod_mk (tc x1 0); simp only [← nhds_prod_eq] at tc
  simp only [ContinuousAt, Complex.ofReal_zero, MulZeroClass.zero_mul] at tc
  have inj := tc.eventually ((s.ray_holomorphic (s.mem_ext c)).along_snd.local_inj
    (s.ray_noncritical_zero c))
  rcases Metric.eventually_nhds_iff.mp inj with ⟨r, rp, inj⟩
  simp only [Real.dist_eq, sub_zero] at inj
  set t := min 1 (r / 2)
  have t0 : 0 < t := lt_min zero_lt_one (half_pos rp)
  have t01 : t ∈ Ioc (0 : ℝ) 1 := mem_Ioc.mpr ⟨t0, min_le_left _ _⟩
  specialize @inj t (by simp only [abs_of_pos t0, min_lt_of_right_lt (half_lt_self rp)]) (h t01)
  exact mul_left_cancel₀ (Complex.ofReal_ne_zero.mpr t0.ne') inj
State after:
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

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 ?_ ?_ ?_
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

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]
State after:
no goals

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 ⊢
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

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
State after:
no goals

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
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

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 ⊢
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

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
State after:
no goals

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
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

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)
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

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
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

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
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

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))
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

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⟩
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

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
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

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)
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

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)
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

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 _ _⟩
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

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)
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

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
State after:
no goals

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)]
State after:
no goals

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
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

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]
State after:
no goals

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⟩
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

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 ⊢
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

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
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

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'
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

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)]
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

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)
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

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)
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

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
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

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
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

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
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

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
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

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
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

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]
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

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])
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

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 ↦ ?_)
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)

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
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)

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)]
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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]
State after:
no goals

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]
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

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 (fun e x => s.ray e (x1 / x0 * x)) y
Tactic:
apply eqn_near
State after:
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

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])
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

State before:
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:
rw [xe]
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 (↑t * x1))) ∈ 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

State before:
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 (↑t * x1))) ∈ 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 e1.self_of_nhds.near
State after:
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

State before:
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:
have xc : ContinuousAt (fun y : ℂ × ℂ ↦ (y.1, x1 / x0 * y.2)) (c, ↑t * x0) :=
  continuousAt_fst.prod (continuousAt_const.mul continuousAt_snd)
State after:
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
xc : ContinuousAt (fun y => (y.1, x1 / x0 * y.2)) (c, ↑t * x0)
⊢ ∀ᶠ (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

State before:
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
xc : ContinuousAt (fun y => (y.1, x1 / x0 * y.2)) (c, ↑t * x0)
⊢ ∀ᶠ (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:
simp only [ContinuousAt] at xc
State after:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, x1 / x0 * (↑t * x0)))
⊢ ∀ᶠ (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

State before:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, x1 / x0 * (↑t * x0)))
⊢ ∀ᶠ (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:
rw [← mul_assoc, mul_comm _ (t:ℂ), mul_assoc, div_mul_cancel₀ _ x00] at xc
State after:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, ↑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

State before:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, ↑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:
refine (xc.eventually e1).mp (eventually_of_forall ?_)
State after:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, ↑t * x1))
⊢ ∀ (x : ℂ × ℂ),
    Eqn s n s.ray (x.1, x1 / x0 * x.2) → s.bottcherNear x.1 ((f x.1)^[n] (s.ray x.1 (x1 / x0 * x.2))) = x.2 ^ d ^ n

State before:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, ↑t * x1))
⊢ ∀ (x : ℂ × ℂ),
    Eqn s n s.ray (x.1, x1 / x0 * x.2) → s.bottcherNear x.1 ((f x.1)^[n] (s.ray x.1 (x1 / x0 * x.2))) = x.2 ^ d ^ n
Tactic:
intro ⟨e, x⟩ e1
State after:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, ↑t * x1))
e x : ℂ
e1 : Eqn s n s.ray ((e, x).1, x1 / x0 * (e, x).2)
⊢ s.bottcherNear (e, x).1 ((f (e, x).1)^[n] (s.ray (e, x).1 (x1 / x0 * (e, x).2))) = (e, x).2 ^ d ^ n

State before:
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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, ↑t * x1))
e x : ℂ
e1 : Eqn s n s.ray ((e, x).1, x1 / x0 * (e, x).2)
⊢ s.bottcherNear (e, x).1 ((f (e, x).1)^[n] (s.ray (e, x).1 (x1 / x0 * (e, x).2))) = (e, x).2 ^ d ^ n
Tactic:
exact _root_.trans e1.eqn (by
  simp only [mul_pow, div_pow, ← de, div_self (pow_ne_zero _ x00), one_mul])
State after:
no goals

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
⊢ ((c, ↑t * x0).1, x1 / x0 * (c, ↑t * x0).2) = (c, ↑t * x1)
Tactic:
simp only [xe]
State after:
no goals

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
xc : Tendsto (fun y => (y.1, x1 / x0 * y.2)) (𝓝 (c, ↑t * x0)) (𝓝 (c, ↑t * x1))
e x : ℂ
e1 : Eqn s n s.ray ((e, x).1, x1 / x0 * (e, x).2)
⊢ ((e, x).1, x1 / x0 * (e, x).2).2 ^ d ^ n = (e, x).2 ^ d ^ n
Tactic:
simp only [mul_pow, div_pow, ← de, div_self (pow_ne_zero _ x00), one_mul]
State after:
no goals

State before:
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
Tactic:
simp only [← hr]
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 c (↑t * x0) = s.ray c (x1 / x0 * (↑t * x0))

State before:
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 c (↑t * x0) = s.ray c (x1 / x0 * (↑t * x0))
Tactic:
rw [xe]
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 c (↑t * x0) = s.ray c (↑t * x1)

State before:
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 c (↑t * x0) = s.ray c (↑t * x1)
Tactic:
exact e
State after:
no goals

State before:
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)
Tactic:
rw [← hr] at e
State after:
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 (fun e x => s.ray e (x1 / x0 * x)) (c, ↑u * x0)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)

State before:
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 (fun e x => s.ray e (x1 / x0 * x)) (c, ↑u * x0)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Tactic:
simp only [uncurry] at e
State after:
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 : s.ray c (↑u * x0) = s.ray c (x1 / x0 * (↑u * x0))
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)

State before:
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 : s.ray c (↑u * x0) = s.ray c (x1 / x0 * (↑u * x0))
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Tactic:
rw [← mul_assoc, mul_comm _ (u:ℂ), mul_assoc, div_mul_cancel₀ _ x00] at e
State after:
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 : s.ray c (↑u * x0) = s.ray c (↑u * x1)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)

State before:
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 : s.ray c (↑u * x0) = s.ray c (↑u * x1)
⊢ s.ray c (↑u * x0) = s.ray c (↑u * x1)
Tactic:
exact e
State after:
no goals

State before:
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
Tactic:
intro t ⟨m, e⟩
State after:
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : t ∈ closure u
⊢ t ∈ u

State before:
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : t ∈ closure u
⊢ t ∈ u
Tactic:
simp only [mem_setOf, mem_closure_iff_frequently] at e ⊢
State after:
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
⊢ t ∈ u

State before:
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
⊢ t ∈ u
Tactic:
have rc : ∀ {x : ℂ}, (c, x) ∈ s.ext → ContinuousAt (fun t : ℝ ↦ s.ray c (↑t * x)) t :=
  fun {x} p ↦
  (s.ray_holomorphic (pt p m)).along_snd.continuousAt.comp_of_eq
    (Complex.continuous_ofReal.continuousAt.mul continuousAt_const) rfl
State after:
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
rc : ∀ {x : ℂ}, (c, x) ∈ s.ext → ContinuousAt (fun t => s.ray c (↑t * x)) t
⊢ t ∈ u

State before:
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)}
t : ℝ
m : t ∈ Ioc 0 1
e : ∃ᶠ (x : ℝ) in 𝓝 t, x ∈ u
rc : ∀ {x : ℂ}, (c, x) ∈ s.ext → ContinuousAt (fun t => s.ray c (↑t * x)) t
⊢ t ∈ u
Tactic:
exact tendsto_nhds_unique_of_frequently_eq (rc p0) (rc p1) e
State after:
no goals