Theorem: GrowOpen.point (Ray/Dynamics/Grow.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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
Tactic:
by_cases za : abs x = 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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : Complex.abs x = 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : ¬Complex.abs x = 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : ¬Complex.abs x = 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
Tactic:
replace za := (Ne.symm za).lt_of_le (Complex.abs.nonneg _)
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
Tactic:
set t := ball (0 : ℂ) 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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
have xt : x ∈ closure t := by
  simp only [closure_ball _ g.pos.ne', mem_closedBall, Complex.dist_eq, sub_zero, ax]
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
have ez : ∃ z : S, MapClusterPt z (𝓝[t] x) (r c) :=
  @exists_clusterPt_of_compactSpace _ _ _ _
    (Filter.map_neBot (hf := mem_closure_iff_nhdsWithin_neBot.mp xt))
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
ez : ∃ z, MapClusterPt z (𝓝[t] x) (r c)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
ez : ∃ z, MapClusterPt z (𝓝[t] x) (r c)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
rcases ez with ⟨z, cp⟩
State after:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
have pz : s.potential c z = abs x := by
  refine eq_of_nhds_neBot (cp.map (Continuous.potential s).along_snd.continuousAt
    (Filter.tendsto_map' ?_))
  have e : ∀ y, y ∈ t → (s.potential c ∘ r c) y = abs y := by
    intro y m; simp only [Function.comp]; exact (g.eqn.self_of_nhdsSet (c, y) ⟨rfl, m⟩).potential
  exact tendsto_nhdsWithin_congr (fun t m ↦ (e t m).symm)
    Complex.continuous_abs.continuousWithinAt
State after:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
rcases s.nice_np c (lt_of_lt_of_le g.post s.p_le_one) z (_root_.trans (le_of_eq pz) ax)
  with ⟨m, nc⟩
State after:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
m : (c, (f c)^[s.np c p] z) ∈ s.near
nc : ∀ (k : ℕ), s.np c p ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
m : (c, (f c)^[s.np c p] z) ∈ s.near
nc : ∀ (k : ℕ), s.np c p ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
replace nc := nc _ (le_refl _)
State after:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
m : (c, (f c)^[s.np c p] z) ∈ s.near
nc : mfderiv I I (s.bottcherNear c) ((f c)^[s.np c p] z) ≠ 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
m : (c, (f c)^[s.np c p] z) ∈ s.near
nc : mfderiv I I (s.bottcherNear c) ((f c)^[s.np c p] z) ≠ 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
generalize hn : s.np c p = n
State after:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
m : (c, (f c)^[s.np c p] z) ∈ s.near
nc : mfderiv I I (s.bottcherNear c) ((f c)^[s.np c p] z) ≠ 0
n : ℕ
hn : s.np c p = n
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
m : (c, (f c)^[s.np c p] z) ∈ s.near
nc : mfderiv I I (s.bottcherNear c) ((f c)^[s.np c p] z) ≠ 0
n : ℕ
hn : s.np c p = n
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
rw [hn] at m nc
State after:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
generalize hb : s.bottcherNearIter n = b
State after:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
have post : Postcritical s c z := lt_of_le_of_lt (_root_.trans (le_of_eq pz) ax) g.post
State after:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
rw [← pz] at za
State after:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
have ba := s.bottcherNearIter_holomorphic m
State after:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
replace nc := s.bottcherNearIter_mfderiv_ne_zero nc (post.not_precritical za.ne')
State after:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
rcases complex_inverse_fun ba nc with ⟨i, ia, ib, bi⟩
State after:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, s.bottcherNearIter n c z)
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (s.bottcherNearIter n x.1 x.2) = x.2
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNearIter n c z), s.bottcherNearIter n x.1 (i x.1 x.2) = x.2
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, s.bottcherNearIter n c z)
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (s.bottcherNearIter n x.1 x.2) = x.2
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNearIter n c z), s.bottcherNearIter n x.1 (i x.1 x.2) = x.2
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
simp only [hb, bz] at ia bi ib
State after:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
have pt : Tendsto (fun p : ℂ × ℂ ↦ (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n)) :=
  continuousAt_fst.prod (continuousAt_snd.pow _)
State after:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
have ian : HolomorphicAt II I (uncurry fun e y : ℂ ↦ i e (y ^ d ^ n)) (c, x) :=
  ia.comp₂_of_eq holomorphicAt_fst holomorphicAt_snd.pow rfl
State after:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y

State before:
case neg.intro.intro.intro.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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ r' c y = r c y
Tactic:
use fun e y ↦ i e (y ^ d ^ 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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n (fun e y => i e (y ^ d ^ n)) y) ∧
    ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y

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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n (fun e y => i e (y ^ d ^ n)) y) ∧
    ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y
Tactic:
constructor
State after:
case h.left
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n (fun e y => i e (y ^ d ^ n)) y

case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : Complex.abs x = 0
⊢ ∃ r', (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r' y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r' c y = r c y
Tactic:
use r
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : Complex.abs x = 0
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r c y = r c y

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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : Complex.abs x = 0
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r c y = r c y
Tactic:
simp only [Complex.abs.eq_zero] at za
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r c y = r c y

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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s (s.np c p) r y) ∧ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ ball 0 p ∧ r c y = r c y
Tactic:
simp only [za, eq_self_iff_true, and_true_iff]
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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, 0), Eqn s (s.np c p) r y) ∧ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p

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 : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, 0), Eqn s (s.np c p) r y) ∧ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p
Tactic:
constructor
State after:
case h.left
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, 0), Eqn s (s.np c p) r y

case h.right
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p

State before:
case h.left
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, 0), Eqn s (s.np c p) r y

case h.right
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p
Tactic:
refine g.eqn.filter_mono (nhds_le_nhdsSet ?_)
State after:
case h.left
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ (c, 0) ∈ {c} ×ˢ ball 0 p

case h.right
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p

State before:
case h.left
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ (c, 0) ∈ {c} ×ˢ ball 0 p

case h.right
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p
Tactic:
exact mk_mem_prod rfl (mem_ball_self g.pos)
State after:
case h.right
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p

State before:
case h.right
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : x = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p
Tactic:
exact (isOpen_ball.eventually_mem (mem_ball_self g.pos)).frequently
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
⊢ x ∈ closure t
Tactic:
simp only [closure_ball _ g.pos.ne', mem_closedBall, Complex.dist_eq, sub_zero, ax]
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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
⊢ s.potential c z = Complex.abs x
Tactic:
refine eq_of_nhds_neBot (cp.map (Continuous.potential s).along_snd.continuousAt
  (Filter.tendsto_map' ?_))
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
⊢ Tendsto (s.potential c ∘ r c) (𝓝[t] x) (𝓝 (Complex.abs x))

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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
⊢ Tendsto (s.potential c ∘ r c) (𝓝[t] x) (𝓝 (Complex.abs x))
Tactic:
have e : ∀ y, y ∈ t → (s.potential c ∘ r c) y = abs y := by
  intro y m; simp only [Function.comp]; exact (g.eqn.self_of_nhdsSet (c, y) ⟨rfl, m⟩).potential
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
e : ∀ y ∈ t, (s.potential c ∘ r c) y = Complex.abs y
⊢ Tendsto (s.potential c ∘ r c) (𝓝[t] x) (𝓝 (Complex.abs x))

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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
e : ∀ y ∈ t, (s.potential c ∘ r c) y = Complex.abs y
⊢ Tendsto (s.potential c ∘ r c) (𝓝[t] x) (𝓝 (Complex.abs x))
Tactic:
exact tendsto_nhdsWithin_congr (fun t m ↦ (e t m).symm)
  Complex.continuous_abs.continuousWithinAt
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✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
⊢ ∀ y ∈ t, (s.potential c ∘ r c) y = Complex.abs y
Tactic:
intro y 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 : ℂ
a z✝ : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
y : ℂ
m : y ∈ t
⊢ (s.potential c ∘ r c) y = Complex.abs y

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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
y : ℂ
m : y ∈ t
⊢ (s.potential c ∘ r c) y = Complex.abs y
Tactic:
simp only [Function.comp]
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
y : ℂ
m : y ∈ t
⊢ s.potential c (r c y) = Complex.abs y

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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
y : ℂ
m : y ∈ t
⊢ s.potential c (r c y) = Complex.abs y
Tactic:
exact (g.eqn.self_of_nhdsSet (c, y) ⟨rfl, m⟩).potential
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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ b c z = x ^ d ^ n
Tactic:
refine eq_of_nhds_neBot (cp.map ?_ (Filter.tendsto_map' ?_))
State after:
case refine_1
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ ContinuousAt (b c) z

case refine_2
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ Tendsto (b c ∘ r c) (𝓝[t] x) (𝓝 (x ^ d ^ n))

State before:
case refine_1
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ ContinuousAt (b c) z
Tactic:
rw [← hb]
State after:
case refine_1
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ ContinuousAt (s.bottcherNearIter n c) z

State before:
case refine_1
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ ContinuousAt (s.bottcherNearIter n c) z
Tactic:
exact (s.bottcherNearIter_holomorphic m).along_snd.continuousAt
State after:
no goals

State before:
case refine_2
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ Tendsto (b c ∘ r c) (𝓝[t] x) (𝓝 (x ^ d ^ n))
Tactic:
have e : ∀ y, y ∈ t → (b c ∘ r c) y = y ^ d ^ n := by
  intro y m
  simp only [Function.comp, ← hb, ← hn]
  exact (g.eqn.self_of_nhdsSet (c, y) ⟨rfl, m⟩).eqn
State after:
case refine_2
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
e : ∀ y ∈ t, (b c ∘ r c) y = y ^ d ^ n
⊢ Tendsto (b c ∘ r c) (𝓝[t] x) (𝓝 (x ^ d ^ n))

State before:
case refine_2
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
e : ∀ y ∈ t, (b c ∘ r c) y = y ^ d ^ n
⊢ Tendsto (b c ∘ r c) (𝓝[t] x) (𝓝 (x ^ d ^ n))
Tactic:
exact tendsto_nhdsWithin_congr (fun t m ↦ (e t m).symm) (continuous_pow _).continuousWithinAt
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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
⊢ ∀ y ∈ t, (b c ∘ r c) y = y ^ d ^ n
Tactic:
intro y 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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
y : ℂ
m : y ∈ t
⊢ (b c ∘ r c) y = y ^ d ^ n

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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
y : ℂ
m : y ∈ t
⊢ (b c ∘ r c) y = y ^ d ^ n
Tactic:
simp only [Function.comp, ← hb, ← hn]
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
y : ℂ
m : y ∈ t
⊢ s.bottcherNearIter (s.np c p) c (r c y) = y ^ d ^ s.np c p

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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
za : 0 < Complex.abs x
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
nc : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
y : ℂ
m : y ∈ t
⊢ s.bottcherNearIter (s.np c p) c (r c y) = y ^ d ^ s.np c p
Tactic:
exact (g.eqn.self_of_nhdsSet (c, y) ⟨rfl, m⟩).eqn
State after:
no goals

State before:
case h.left
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n (fun e y => i e (y ^ d ^ n)) y
Tactic:
apply eqn_near ian
State after:
case h.left.mem
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (c, (f c)^[n] (i c (x ^ d ^ n))) ∈ s.near

case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (i y.1 (y.2 ^ d ^ n))) = y.2 ^ d ^ n

State before:
case h.left.mem
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (c, (f c)^[n] (i c (x ^ d ^ n))) ∈ s.near
Tactic:
simp only [←bz]
State after:
case h.left.mem
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (c, (f c)^[n] (i c (b c z))) ∈ s.near

State before:
case h.left.mem
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (c, (f c)^[n] (i c (b c z))) ∈ s.near
Tactic:
rw [ib.self_of_nhds]
State after:
case h.left.mem
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (c, (f c)^[n] (c, z).2) ∈ s.near

State before:
case h.left.mem
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ (c, (f c)^[n] (c, z).2) ∈ s.near
Tactic:
exact m
State after:
no goals

State before:
case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (i y.1 (y.2 ^ d ^ n))) = y.2 ^ d ^ n
Tactic:
refine (pt.eventually bi).mp (eventually_of_forall ?_)
State after:
case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∀ (x : ℂ × ℂ),
    b (x.1, x.2 ^ d ^ n).1 (i (x.1, x.2 ^ d ^ n).1 (x.1, x.2 ^ d ^ n).2) = (x.1, x.2 ^ d ^ n).2 →
      s.bottcherNear x.1 ((f x.1)^[n] (i x.1 (x.2 ^ d ^ n))) = x.2 ^ d ^ n

State before:
case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∀ (x : ℂ × ℂ),
    b (x.1, x.2 ^ d ^ n).1 (i (x.1, x.2 ^ d ^ n).1 (x.1, x.2 ^ d ^ n).2) = (x.1, x.2 ^ d ^ n).2 →
      s.bottcherNear x.1 ((f x.1)^[n] (i x.1 (x.2 ^ d ^ n))) = x.2 ^ d ^ n
Tactic:
intro _ bi
State after:
case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
x✝ : ℂ × ℂ
bi : b (x✝.1, x✝.2 ^ d ^ n).1 (i (x✝.1, x✝.2 ^ d ^ n).1 (x✝.1, x✝.2 ^ d ^ n).2) = (x✝.1, x✝.2 ^ d ^ n).2
⊢ s.bottcherNear x✝.1 ((f x✝.1)^[n] (i x✝.1 (x✝.2 ^ d ^ n))) = x✝.2 ^ d ^ n

State before:
case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
x✝ : ℂ × ℂ
bi : b (x✝.1, x✝.2 ^ d ^ n).1 (i (x✝.1, x✝.2 ^ d ^ n).1 (x✝.1, x✝.2 ^ d ^ n).2) = (x✝.1, x✝.2 ^ d ^ n).2
⊢ s.bottcherNear x✝.1 ((f x✝.1)^[n] (i x✝.1 (x✝.2 ^ d ^ n))) = x✝.2 ^ d ^ n
Tactic:
simp only [← hb] at bi
State after:
case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
x✝ : ℂ × ℂ
bi : s.bottcherNearIter n x✝.1 (i x✝.1 (x✝.2 ^ d ^ n)) = x✝.2 ^ d ^ n
⊢ s.bottcherNear x✝.1 ((f x✝.1)^[n] (i x✝.1 (x✝.2 ^ d ^ n))) = x✝.2 ^ d ^ n

State before:
case h.left.loc
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
x✝ : ℂ × ℂ
bi : s.bottcherNearIter n x✝.1 (i x✝.1 (x✝.2 ^ d ^ n)) = x✝.2 ^ d ^ n
⊢ s.bottcherNear x✝.1 ((f x✝.1)^[n] (i x✝.1 (x✝.2 ^ d ^ n))) = x✝.2 ^ d ^ n
Tactic:
exact bi
State after:
no goals

State before:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y
Tactic:
have ne : MapClusterPt (z, z) (𝓝[t] x) fun y ↦ (r c y, i c (y ^ d ^ n)) := by
  apply cp.prod; refine Filter.Tendsto.mono_left ?_ nhdsWithin_le_nhds
  have ic := ian.along_snd.continuousAt
  simp only [ContinuousAt, ←bz] at ic; rw [ib.self_of_nhds] at ic
  exact ic
State after:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y

State before:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y
Tactic:
have inj := (@Filter.Eventually.frequently _ _ ne _
        (Filter.Eventually.filter_mono inf_le_left (ba.along_snd.local_inj nc))).filter_mono
    inf_le_right
State after:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : S × S) in Filter.map (fun y => (r c y, i c (y ^ d ^ n))) (𝓝[t] x),
    s.bottcherNearIter n c x.1 = s.bottcherNearIter n c x.2 → x.1 = x.2
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y

State before:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : S × S) in Filter.map (fun y => (r c y, i c (y ^ d ^ n))) (𝓝[t] x),
    s.bottcherNearIter n c x.1 = s.bottcherNearIter n c x.2 → x.1 = x.2
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y
Tactic:
simp only [Filter.frequently_map, frequently_nhdsWithin_iff] at inj
State after:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y

State before:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∃ᶠ (y : ℂ) in 𝓝 x, y ∈ t ∧ i c (y ^ d ^ n) = r c y
Tactic:
apply inj.mp
State after:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t →
      x ∈ t ∧ i c (x ^ d ^ n) = r c x

State before:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t →
      x ∈ t ∧ i c (x ^ d ^ n) = r c x
Tactic:
apply ((continuousAt_const.prod (continuousAt_pow _ _)).eventually bi).mp
State after:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 x,
    b (c, x ^ d ^ n).1 (i (c, x ^ d ^ n).1 (c, x ^ d ^ n).2) = (c, x ^ d ^ n).2 →
      (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t →
        x ∈ t ∧ i c (x ^ d ^ n) = r c x

State before:
case h.right
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ᶠ (x : ℂ) in 𝓝 x,
    b (c, x ^ d ^ n).1 (i (c, x ^ d ^ n).1 (c, x ^ d ^ n).2) = (c, x ^ d ^ n).2 →
      (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t →
        x ∈ t ∧ i c (x ^ d ^ n) = r c x
Tactic:
apply eventually_of_forall
State after:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ (x : ℂ),
    b (c, x ^ d ^ n).1 (i (c, x ^ d ^ n).1 (c, x ^ d ^ n).2) = (c, x ^ d ^ n).2 →
      (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t →
        x ∈ t ∧ i c (x ^ d ^ n) = r c x

State before:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ (x : ℂ),
    b (c, x ^ d ^ n).1 (i (c, x ^ d ^ n).1 (c, x ^ d ^ n).2) = (c, x ^ d ^ n).2 →
      (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t →
        x ∈ t ∧ i c (x ^ d ^ n) = r c x
Tactic:
simp only [← hb, ← hn]
State after:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ (x : ℂ),
    s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p →
      (s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
            r c x = i c (x ^ d ^ s.np c p)) ∧
          x ∈ t →
        x ∈ t ∧ i c (x ^ d ^ s.np c p) = r c x

State before:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ne : MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
inj :
  ∃ᶠ (x : ℂ) in 𝓝 x,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
⊢ ∀ (x : ℂ),
    s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p →
      (s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
            r c x = i c (x ^ d ^ s.np c p)) ∧
          x ∈ t →
        x ∈ t ∧ i c (x ^ d ^ s.np c p) = r c x
Tactic:
intro x bi ⟨inj, m⟩
State after:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x✝ : ℂ
ax : Complex.abs x✝ ≤ p
t : Set ℂ := ball 0 p
xt : x✝ ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x✝) (r c)
pz : s.potential c z = Complex.abs x✝
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x✝ ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x✝ ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x✝ ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x✝)) (𝓝 (c, x✝ ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x✝)
ne : MapClusterPt (z, z) (𝓝[t] x✝) fun y => (r c y, i c (y ^ d ^ n))
inj✝ :
  ∃ᶠ (x : ℂ) in 𝓝 x✝,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
x : ℂ
bi : s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p
inj :
  s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
    r c x = i c (x ^ d ^ s.np c p)
m : x ∈ t
⊢ x ∈ t ∧ i c (x ^ d ^ s.np c p) = r c x

State before:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x✝ : ℂ
ax : Complex.abs x✝ ≤ p
t : Set ℂ := ball 0 p
xt : x✝ ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x✝) (r c)
pz : s.potential c z = Complex.abs x✝
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x✝ ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x✝ ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x✝ ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x✝)) (𝓝 (c, x✝ ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x✝)
ne : MapClusterPt (z, z) (𝓝[t] x✝) fun y => (r c y, i c (y ^ d ^ n))
inj✝ :
  ∃ᶠ (x : ℂ) in 𝓝 x✝,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
x : ℂ
bi : s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p
inj :
  s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
    r c x = i c (x ^ d ^ s.np c p)
m : x ∈ t
⊢ x ∈ t ∧ i c (x ^ d ^ s.np c p) = r c x
Tactic:
refine ⟨m, (inj ?_).symm⟩
State after:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x✝ : ℂ
ax : Complex.abs x✝ ≤ p
t : Set ℂ := ball 0 p
xt : x✝ ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x✝) (r c)
pz : s.potential c z = Complex.abs x✝
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x✝ ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x✝ ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x✝ ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x✝)) (𝓝 (c, x✝ ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x✝)
ne : MapClusterPt (z, z) (𝓝[t] x✝) fun y => (r c y, i c (y ^ d ^ n))
inj✝ :
  ∃ᶠ (x : ℂ) in 𝓝 x✝,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
x : ℂ
bi : s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p
inj :
  s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
    r c x = i c (x ^ d ^ s.np c p)
m : x ∈ t
⊢ s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p))

State before:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x✝ : ℂ
ax : Complex.abs x✝ ≤ p
t : Set ℂ := ball 0 p
xt : x✝ ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x✝) (r c)
pz : s.potential c z = Complex.abs x✝
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x✝ ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x✝ ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x✝ ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x✝)) (𝓝 (c, x✝ ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x✝)
ne : MapClusterPt (z, z) (𝓝[t] x✝) fun y => (r c y, i c (y ^ d ^ n))
inj✝ :
  ∃ᶠ (x : ℂ) in 𝓝 x✝,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
x : ℂ
bi : s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p
inj :
  s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
    r c x = i c (x ^ d ^ s.np c p)
m : x ∈ t
⊢ s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p))
Tactic:
simp only [bi]
State after:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x✝ : ℂ
ax : Complex.abs x✝ ≤ p
t : Set ℂ := ball 0 p
xt : x✝ ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x✝) (r c)
pz : s.potential c z = Complex.abs x✝
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x✝ ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x✝ ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x✝ ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x✝)) (𝓝 (c, x✝ ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x✝)
ne : MapClusterPt (z, z) (𝓝[t] x✝) fun y => (r c y, i c (y ^ d ^ n))
inj✝ :
  ∃ᶠ (x : ℂ) in 𝓝 x✝,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
x : ℂ
bi : s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p
inj :
  s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
    r c x = i c (x ^ d ^ s.np c p)
m : x ∈ t
⊢ s.bottcherNearIter (s.np c p) c (r c x) = x ^ d ^ s.np c p

State before:
case h.right.hp
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x✝ : ℂ
ax : Complex.abs x✝ ≤ p
t : Set ℂ := ball 0 p
xt : x✝ ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x✝) (r c)
pz : s.potential c z = Complex.abs x✝
n : ℕ
m✝ : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x✝ ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x✝ ^ d ^ n)
bi✝ : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x✝ ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x✝)) (𝓝 (c, x✝ ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x✝)
ne : MapClusterPt (z, z) (𝓝[t] x✝) fun y => (r c y, i c (y ^ d ^ n))
inj✝ :
  ∃ᶠ (x : ℂ) in 𝓝 x✝,
    (s.bottcherNearIter n c (r c x) = s.bottcherNearIter n c (i c (x ^ d ^ n)) → r c x = i c (x ^ d ^ n)) ∧ x ∈ t
x : ℂ
bi : s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) = x ^ d ^ s.np c p
inj :
  s.bottcherNearIter (s.np c p) c (r c x) = s.bottcherNearIter (s.np c p) c (i c (x ^ d ^ s.np c p)) →
    r c x = i c (x ^ d ^ s.np c p)
m : x ∈ t
⊢ s.bottcherNearIter (s.np c p) c (r c x) = x ^ d ^ s.np c p
Tactic:
exact (g.eqn.self_of_nhdsSet ⟨c, x⟩ (mk_mem_prod rfl m)).eqn
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✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ MapClusterPt (z, z) (𝓝[t] x) fun y => (r c y, i c (y ^ d ^ n))
Tactic:
apply cp.prod
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝[t] 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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝[t] x) (𝓝 z)
Tactic:
refine Filter.Tendsto.mono_left ?_ nhdsWithin_le_nhds
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
have ic := ian.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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : ContinuousAt (fun y => i c (y ^ d ^ n)) x
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : ContinuousAt (fun y => i c (y ^ d ^ n)) x
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
simp only [ContinuousAt, ←bz] at ic
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (i c (b c z)))
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (i c (b c z)))
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
rw [ib.self_of_nhds] at ic
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✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (c, z).2)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 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 : ℂ
a z✝ : S
d n✝ : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
g : GrowOpen s c p r
inst✝ : OnePreimage s
x : ℂ
ax : Complex.abs x ≤ p
t : Set ℂ := ball 0 p
xt : x ∈ closure t
z : S
za : 0 < s.potential c z
cp : MapClusterPt z (𝓝[t] x) (r c)
pz : s.potential c z = Complex.abs x
n : ℕ
m : (c, (f c)^[n] z) ∈ s.near
hn : s.np c p = n
b : ℂ → S → ℂ
hb : s.bottcherNearIter n = b
bz : b c z = x ^ d ^ n
post : Postcritical s c z
ba : HolomorphicAt (I.prod I) I (uncurry (s.bottcherNearIter n)) (c, z)
nc : mfderiv I I (s.bottcherNearIter n c) z ≠ 0
i : ℂ → ℂ → S
ia : HolomorphicAt (I.prod I) I (uncurry i) (c, x ^ d ^ n)
bi : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, x ^ d ^ n), b x.1 (i x.1 x.2) = x.2
ib : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), i x.1 (b x.1 x.2) = x.2
pt : Tendsto (fun p => (p.1, p.2 ^ d ^ n)) (𝓝 (c, x)) (𝓝 (c, x ^ d ^ n))
ian : HolomorphicAt (I.prod I) I (uncurry fun e y => i e (y ^ d ^ n)) (c, x)
ic : Tendsto (fun y => i c (y ^ d ^ n)) (𝓝 x) (𝓝 (c, z).2)
⊢ Tendsto (fun x => i c (x ^ d ^ n)) (𝓝 x) (𝓝 z)
Tactic:
exact ic
State after:
no goals