internlm/Lean-Github huggingface dataset:
Theorem: GrowOpen.point
Proof 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 _)
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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]
Proof 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
Theorem: GrowOpen.point
Proof 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))
Proof 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
Theorem: GrowOpen.point
Proof 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⟩
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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⟩
Proof 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
Theorem: GrowOpen.point
Proof 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 _)
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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
Proof 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
Theorem: GrowOpen.point
Proof 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')
Proof 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
Theorem: GrowOpen.point
Proof 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⟩
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, 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