Theorem: Super.bottcher_eqn (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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
have h0 : ∀ {c z}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d := by
  intro c z m
  suffices e : ∀ᶠ w in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d by
    refine (HolomorphicOn.eq_of_locally_eq ?_ (fun z m ↦
      (s.bottcher_holomorphicOn (c, z) m).along_snd.pow) (s.post_slice_connected c).isPreconnected
      ⟨a, s.post_a c, e⟩).self_of_nhdsSet m
    intro z m
    exact (s.bottcher_holomorphicOn _ (s.stays_post m)).along_snd.comp (s.fa _).along_snd
  have e := s.bottcher_eq_bottcherNear c
  have fc := (s.fa (c, a)).along_snd.continuousAt; simp only [ContinuousAt, s.f0] at fc
  apply e.mp; apply (fc.eventually e).mp
  apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near c)).mp
  refine eventually_of_forall fun w m e0 e1 ↦ ?_; simp only at m e0 e1
  simp only [e0, e1]; exact s.bottcherNear_eqn 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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
by_cases p : (c, z) ∈ s.post
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

case neg
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

case neg
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
simp only [h0 p]
State after:
case neg
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
by_cases m : (c, z) ∈ s.basin
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

case neg
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∉ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∉ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
have m1 : (c, f c z) ∉ s.basin := by
  contrapose m; simp only [not_not] at m ⊢
  rcases m with ⟨n, m⟩; use n + 1; simp only at m ⊢; rwa [Function.iterate_succ_apply]
State after:
case neg
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∉ s.basin
m1 : (c, f c z) ∉ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∉ s.basin
m1 : (c, f c z) ∉ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
simp only [s.bottcher_not_basin m, s.bottcher_not_basin m1, one_pow]
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
suffices e : ∀ᶠ w in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d by
  refine (HolomorphicOn.eq_of_locally_eq ?_ (fun z m ↦
    (s.bottcher_holomorphicOn (c, z) m).along_snd.pow) (s.post_slice_connected c).isPreconnected
    ⟨a, s.post_a c, e⟩).self_of_nhdsSet m
  intro z m
  exact (s.bottcher_holomorphicOn _ (s.stays_post m)).along_snd.comp (s.fa _).along_snd
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
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d

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
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
have e := s.bottcher_eq_bottcherNear c
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
have fc := (s.fa (c, a)).along_snd.continuousAt
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : ContinuousAt (fun y => f c y) a
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : ContinuousAt (fun y => f c y) a
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
simp only [ContinuousAt, s.f0] at fc
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
apply e.mp
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (x : S) in 𝓝 a, s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (x : S) in 𝓝 a, s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d
Tactic:
apply (fc.eventually e).mp
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (x : S) in 𝓝 a,
    s.bottcher c (f c x) = s.bottcherNear c (f c x) →
      s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (x : S) in 𝓝 a,
    s.bottcher c (f c x) = s.bottcherNear c (f c x) →
      s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d
Tactic:
apply ((s.isOpen_near.snd_preimage c).eventually_mem (s.mem_near c)).mp
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (x : S) in 𝓝 a,
    x ∈ {b | (c, b) ∈ s.near} →
      s.bottcher c (f c x) = s.bottcherNear c (f c x) →
        s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
⊢ ∀ᶠ (x : S) in 𝓝 a,
    x ∈ {b | (c, b) ∈ s.near} →
      s.bottcher c (f c x) = s.bottcherNear c (f c x) →
        s.bottcher c x = s.bottcherNear c x → s.bottcher c (f c x) = s.bottcher c x ^ d
Tactic:
refine eventually_of_forall fun w m e0 e1 ↦ ?_
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcher c (f c w) = s.bottcher c w ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcher c (f c w) = s.bottcher c w ^ d
Tactic:
simp only [e0, e1]
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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcherNear c (f c w) = s.bottcherNear c w ^ d

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
e : ∀ᶠ (z : S) in 𝓝 a, s.bottcher c z = s.bottcherNear c z
fc : Tendsto (fun y => f c y) (𝓝 a) (𝓝 a)
w : S
m : w ∈ {b | (c, b) ∈ s.near}
e0 : s.bottcher c (f c w) = s.bottcherNear c (f c w)
e1 : s.bottcher c w = s.bottcherNear c w
⊢ s.bottcherNear c (f c w) = s.bottcherNear c w ^ d
Tactic:
exact s.bottcherNear_eqn m
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✝ 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
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
refine (HolomorphicOn.eq_of_locally_eq ?_ (fun z m ↦
  (s.bottcher_holomorphicOn (c, z) m).along_snd.pow) (s.post_slice_connected c).isPreconnected
  ⟨a, s.post_a c, e⟩).self_of_nhdsSet 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
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
⊢ HolomorphicOn I I (fun x => s.bottcher c (f c x)) fun z => s.post (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
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
⊢ HolomorphicOn I I (fun x => s.bottcher c (f c x)) fun z => s.post (c, z)
Tactic:
intro 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
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
z : S
m : z ∈ fun z => s.post (c, z)
⊢ HolomorphicAt I I (fun x => s.bottcher c (f c x)) 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
e : ∀ᶠ (w : S) in 𝓝 a, s.bottcher c (f c w) = s.bottcher c w ^ d
z : S
m : z ∈ fun z => s.post (c, z)
⊢ HolomorphicAt I I (fun x => s.bottcher c (f c x)) z
Tactic:
exact (s.bottcher_holomorphicOn _ (s.stays_post m)).along_snd.comp (s.fa _).along_snd
State after:
no goals

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
have e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post := s.basin_post m
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
have e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post := by
  rcases e0 with ⟨n, e0⟩; use n
  simp only [← Function.iterate_succ_apply, Function.iterate_succ_apply']
  exact s.stays_post e0
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ s.bottcher c (f c z) = s.bottcher c z ^ d
Tactic:
simp only [Super.bottcher, e0, e1, dif_pos]
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] z)) ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] z)) ^ d
Tactic:
generalize hk0 : Nat.find e0 = k0
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
⊢ (fun w => w ^ (↑d)⁻¹)^[Nat.find ⋯] (s.bottcherPost c ((f c)^[Nat.find ⋯] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d
Tactic:
generalize hk1 : Nat.find e1 = k1
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c ((f c)^[k1] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
kk : k0 = k1 + 1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c ((f c)^[k1] (f c z))) =
    (fun w => w ^ (↑d)⁻¹)^[k0] (s.bottcherPost c ((f c)^[k0] z)) ^ d
Tactic:
simp only [kk, ← Function.iterate_succ_apply, Function.iterate_succ_apply']
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
kk : k0 = k1 + 1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) =
    ((fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) ^ (↑d)⁻¹) ^ d

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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
kk : k0 = k1 + 1
⊢ (fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) =
    ((fun w => w ^ (↑d)⁻¹)^[k1] (s.bottcherPost c (f c ((f c)^[k1] z))) ^ (↑d)⁻¹) ^ d
Tactic:
rw [Complex.cpow_nat_inv_pow _ s.d0]
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
Tactic:
rcases e0 with ⟨n, e0⟩
State after:
case intro
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post

State before:
case intro
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
Tactic:
use n
State after:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, (f c)^[n] (f c z)) ∈ s.post

State before:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, (f c)^[n] (f c z)) ∈ s.post
Tactic:
simp only [← Function.iterate_succ_apply, Function.iterate_succ_apply']
State after:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, f c ((f c)^[n] z)) ∈ s.post

State before:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
n : ℕ
e0 : (c, (f c)^[n] z) ∈ s.post
⊢ (c, f c ((f c)^[n] z)) ∈ s.post
Tactic:
exact s.stays_post e0
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ k0 = k1 + 1
Tactic:
rw [← hk0, ← hk1]
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 = Nat.find e1 + 1

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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 = Nat.find e1 + 1
Tactic:
apply le_antisymm
State after:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 ≤ Nat.find e1 + 1

case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e1 + 1 ≤ Nat.find e0

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e0 ≤ Nat.find e1 + 1
Tactic:
apply Nat.find_le
State after:
case a.hn
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1 + 1] z) ∈ s.post

State before:
case a.hn
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1 + 1] z) ∈ s.post
Tactic:
simp only [Function.iterate_succ_apply]
State after:
case a.hn
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1] (f c z)) ∈ s.post

State before:
case a.hn
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ (c, (f c)^[Nat.find e1] (f c z)) ∈ s.post
Tactic:
exact Nat.find_spec e1
State after:
no goals

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ Nat.find e1 + 1 ≤ Nat.find e0
Tactic:
rw [Nat.succ_le_iff, Nat.lt_find_iff]
State after:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ ∀ m ≤ Nat.find e1, (c, (f c)^[m] z) ∉ s.post

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
⊢ ∀ m ≤ Nat.find e1, (c, (f c)^[m] z) ∉ s.post
Tactic:
intro n n1
State after:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : n ≤ Nat.find e1
⊢ (c, (f c)^[n] z) ∉ s.post

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : n ≤ Nat.find e1
⊢ (c, (f c)^[n] z) ∉ s.post
Tactic:
contrapose n1
State after:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : ¬(c, (f c)^[n] z) ∉ s.post
⊢ ¬n ≤ Nat.find e1

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : ¬(c, (f c)^[n] z) ∉ s.post
⊢ ¬n ≤ Nat.find e1
Tactic:
simp only [not_not, not_le] at n1 ⊢
State after:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
⊢ Nat.find e1 < n

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
⊢ Nat.find e1 < n
Tactic:
have n0 : n ≠ 0 := by
  contrapose p; simp only [not_not] at p ⊢
  simp only [p, Function.iterate_zero_apply] at n1; exact n1
State after:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 < n

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 < n
Tactic:
rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← Nat.sub_add_cancel (Nat.pos_of_ne_zero n0)]
State after:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 + 1 ≤ n - Nat.succ 0 + Nat.succ 0

State before:
case a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 + 1 ≤ n - Nat.succ 0 + Nat.succ 0
Tactic:
apply Nat.succ_le_succ
State after:
case a.a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 ≤ n - Nat.succ 0

State before:
case a.a
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ Nat.find e1 ≤ n - Nat.succ 0
Tactic:
apply Nat.find_le
State after:
case a.a.hn
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ (c, (f c)^[n - Nat.succ 0] (f c z)) ∈ s.post

State before:
case a.a.hn
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
n0 : n ≠ 0
⊢ (c, (f c)^[n - Nat.succ 0] (f c z)) ∈ s.post
Tactic:
simp only [← Function.iterate_succ_apply, Nat.succ_eq_add_one,
  Nat.sub_add_cancel (Nat.pos_of_ne_zero n0), n1, zero_add]
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 x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
⊢ n ≠ 0
Tactic:
contrapose p
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : ¬n ≠ 0
⊢ ¬(c, z) ∉ s.post

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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : ¬n ≠ 0
⊢ ¬(c, z) ∉ s.post
Tactic:
simp only [not_not] at p ⊢
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : n = 0
⊢ (c, z) ∈ s.post

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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
n1 : (c, (f c)^[n] z) ∈ s.post
p : n = 0
⊢ (c, z) ∈ s.post
Tactic:
simp only [p, Function.iterate_zero_apply] at n1
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
p : n = 0
n1 : (c, z) ∈ s.post
⊢ (c, z) ∈ s.post

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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
m : (c, z) ∈ s.basin
e0 : ∃ n, (c, (f c)^[n] z) ∈ s.post
e1 : ∃ n, (c, (f c)^[n] (f c z)) ∈ s.post
k0 : ℕ
hk0 : Nat.find e0 = k0
k1 : ℕ
hk1 : Nat.find e1 = k1
n : ℕ
p : n = 0
n1 : (c, z) ∈ s.post
⊢ (c, z) ∈ s.post
Tactic:
exact n1
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, z) ∉ s.basin
⊢ (c, f c z) ∉ s.basin
Tactic:
contrapose 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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : ¬(c, f c z) ∉ s.basin
⊢ ¬(c, z) ∉ s.basin

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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : ¬(c, f c z) ∉ s.basin
⊢ ¬(c, z) ∉ s.basin
Tactic:
simp only [not_not] at 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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, f c z) ∈ s.basin
⊢ (c, z) ∈ s.basin

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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
m : (c, f c z) ∈ s.basin
⊢ (c, z) ∈ s.basin
Tactic:
rcases m with ⟨n, m⟩
State after:
case intro
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ (c, z) ∈ s.basin

State before:
case intro
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ (c, z) ∈ s.basin
Tactic:
use n + 1
State after:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ ((c, z).1, (f (c, z).1)^[n + 1] (c, z).2) ∈ s.near

State before:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
n : ℕ
m : ((c, f c z).1, (f (c, f c z).1)^[n] (c, f c z).2) ∈ s.near
⊢ ((c, z).1, (f (c, z).1)^[n + 1] (c, z).2) ∈ s.near
Tactic:
simp only at m ⊢
State after:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
n : ℕ
m : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near

State before:
case h
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
h0 : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → s.bottcher c (f c z) = s.bottcher c z ^ d
p : (c, z) ∉ s.post
n : ℕ
m : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ (c, (f c)^[n + 1] z) ∈ s.near
Tactic:
rwa [Function.iterate_succ_apply]
State after:
no goals