internlm/Lean-Github huggingface dataset:
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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 _)
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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)
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
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
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
Proof 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
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
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]
Proof 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
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
za : x = 0
⊢ (∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, 0), Eqn s (s.np c p) r y) ∧ ∃ᶠ (y : ℂ) in 𝓝 0, y ∈ ball 0 p
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
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
Theorem: GrowOpen.point
Proof 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 ?_)
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
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
Theorem: GrowOpen.point
Proof 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)
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof state after:
no goals
Theorem: GrowOpen.point
Proof 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]
Proof state after:
no goals
Theorem: GrowOpen.point
Proof 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' ?_))
Proof 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))
Theorem: GrowOpen.point
Proof 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
Proof 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))
Theorem: GrowOpen.point
Proof 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
Proof state after:
no goals
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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]
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof state after:
no goals
Theorem: GrowOpen.point
Proof 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' ?_))
Proof 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))