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