Theorem: Super.bottcher_holomorphicOn (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
⊢ HolomorphicOn (I.prod I) I (uncurry s.bottcher) s.post
Tactic:
intro ⟨c, z⟩ 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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcher) (c, z)

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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ HolomorphicAt (I.prod I) I (uncurry s.bottcher) (c, z)
Tactic:
apply ((choose_spec s.ray_inv).1 _ m).congr
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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ (𝓝 (c, z)).EventuallyEq (uncurry (choose ⋯)) (uncurry s.bottcher)

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
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ (𝓝 (c, z)).EventuallyEq (uncurry (choose ⋯)) (uncurry s.bottcher)
Tactic:
exact s.eqOn_bottcher_bottcherPost.symm.eventuallyEq_of_mem (s.isOpen_post.mem_nhds m)
State after:
no goals