Theorem: GrowOpen.point
Proof 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
Proof 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