Theorem: Super.ray_inv (Ray/Dynamics/Bottcher.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
⊢ ∃ b, HolomorphicOn (I.prod I) I (uncurry b) s.post ∧ ∀ y ∈ s.ext, b y.1 (s.ray y.1 y.2) = y.2
Tactic:
rw [← s.ray_bij.image_eq]
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
⊢ ∃ b,
    HolomorphicOn (I.prod I) I (uncurry b) ((fun y => (y.1, s.ray y.1 y.2)) '' s.ext) ∧
      ∀ y ∈ s.ext, b y.1 (s.ray y.1 y.2) = y.2

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
⊢ ∃ b,
    HolomorphicOn (I.prod I) I (uncurry b) ((fun y => (y.1, s.ray y.1 y.2)) '' s.ext) ∧
      ∀ y ∈ s.ext, b y.1 (s.ray y.1 y.2) = y.2
Tactic:
exact global_complex_inverse_fun_open s.ray_holomorphicOn (fun _ m ↦ s.ray_noncritical m)
    s.ray_bij.injOn s.isOpen_ext
State after:
no goals