Theorem: Super.bottcherNearIter_nontrivial_a (Ray/Dynamics/BottcherNearM.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 : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (s.bottcherNear c) ((f c)^[n] a)
Tactic:
simp only [s.iter_a]
State after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (s.bottcherNear c) a

State before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (s.bottcherNear c) a
Tactic:
exact nontrivialHolomorphicAt_of_mfderiv_ne_zero
  (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd
  (s.bottcherNear_mfderiv_ne_zero c)
State after:
no goals