Theorem: bottcher_analytic (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ AnalyticOn ℂ (bottcher' d) (multibrot d)ᶜ
Tactic:
set s := superF d
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ AnalyticOn ℂ (bottcher' d) (multibrot d)ᶜ

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ AnalyticOn ℂ (bottcher' d) (multibrot d)ᶜ
Tactic:
intro c m
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ AnalyticAt ℂ (bottcher' d) c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ AnalyticAt ℂ (bottcher' d) c
Tactic:
apply HolomorphicAt.analyticAt I I
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ HolomorphicAt I I (bottcher' d) c

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ HolomorphicAt I I (bottcher' d) c
Tactic:
exact (s.bottcher_holomorphicOn (c, c) (multibrotPost m)).comp₂_of_eq holomorphicAt_id
  (holomorphic_coe _) rfl
State after:
no goals