Theorem: rayHolomorphic (Ray/Dynamics/Multibrot/Isomorphism.lean)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (ray d) (ball 0 1)
Tactic:
rw [← bottcher_surj d]
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (ray d) (bottcher d '' multibrotExt d)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (ray d) (bottcher d '' multibrotExt d)
Tactic:
exact (Classical.choose_spec (ray_exists d)).1
State after:
no goals