Theorem: Super.bottcherNearIterNontrivial (Ray/Dynamics/Postcritical.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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
rcases((Filter.eventually_ge_atTop n).and (s.eventually_noncritical ⟨_, r⟩)).exists with
  ⟨m, nm, mc⟩
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
have r' := s.iter_stays_near' r nm
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : NontrivialHolomorphicAt (s.bottcherNearIter m c) z
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
replace h := h.nonconst
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
refine ⟨(s.bottcherNearIter_holomorphic r).along_snd, ?_⟩
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z
Tactic:
contrapose h
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
Tactic:
simp only [Filter.not_frequently, not_not] at h ⊢
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter m c x = s.bottcherNearIter m c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter m c x = s.bottcherNearIter m c z
Tactic:
rw [← Nat.sub_add_cancel nm]
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (m - n + n) c x = s.bottcherNearIter (m - n + n) c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (m - n + n) c x = s.bottcherNearIter (m - n + n) c z
Tactic:
generalize hk : m - n = k
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
hk : m - n = k
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
hk : m - n = k
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
clear hk nm mc r' p m
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
have er : ∀ᶠ w in 𝓝 z, (c, (f c)^[n] w) ∈ s.near :=
  (continuousAt_const.prod (s.continuousAt_iter continuousAt_const
    continuousAt_id)).eventually_mem (s.isOpen_near.mem_nhds r)
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
refine (h.and er).mp (eventually_of_forall ?_)
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ (x : S),
    s.bottcherNearIter n c x = s.bottcherNearIter n c z ∧ (c, (f c)^[n] x) ∈ s.near →
      s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ (x : S),
    s.bottcherNearIter n c x = s.bottcherNearIter n c z ∧ (c, (f c)^[n] x) ∈ s.near →
      s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
intro x ⟨e, m⟩
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNearIter n c x = s.bottcherNearIter n c z
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNearIter n c x = s.bottcherNearIter n c z
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
simp only [Super.bottcherNearIter] at e
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNear c ((f c)^[n] x) = s.bottcherNear c ((f c)^[n] z)
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNear c ((f c)^[n] x) = s.bottcherNear c ((f c)^[n] z)
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
simp only [Super.bottcherNearIter, Function.iterate_add_apply, s.bottcherNear_eqn_iter m,
  s.bottcherNear_eqn_iter r, e]
State after:
no goals

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 z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Tactic:
by_cases p0 : s.potential c z = 0
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : ¬s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Tactic:
rw [s.potential_eq_zero_of_onePreimage] at p0
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Tactic:
rw [p0]
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) a

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) a
Tactic:
exact s.bottcherNearIter_nontrivial_a
State after:
no goals

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
p0 : ¬s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Tactic:
exact nontrivialHolomorphicAt_of_mfderiv_ne_zero (s.bottcherNearIter_holomorphic r').along_snd
    (s.bottcherNearIter_mfderiv_ne_zero mc (p.not_precritical p0))
State after:
no goals