internlm/Lean-Github huggingface dataset:
Theorem: Super.grow_start
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r (c, a).1 (s.bottcherNear (c, a).1 (c, a).2) = (c, a).2
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near
Tactic:
simp only [s.bottcherNear_a] at r0
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near
Theorem: Super.grow_start
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near
Tactic:
simp only [uncurry, r0]
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ (c, a) ∈ s.near
Theorem: Super.grow_start
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
r0 : r c 0 = a
⊢ (c, a) ∈ s.near
Tactic:
exact s.mem_near c
Proof state after:
no goals
Theorem: Super.grow_start
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
Tactic:
rw [isOpen_ball.mem_nhdsSet, ← ball_prod_same]
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ {c} ×ˢ closedBall 0 (p / 2) ⊆ ball c p ×ˢ ball 0 p
Theorem: Super.grow_start
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ {c} ×ˢ closedBall 0 (p / 2) ⊆ ball c p ×ˢ ball 0 p
Tactic:
apply prod_mono
Proof state after:
case hs
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ {c} ⊆ ball c p

case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p
Theorem: Super.grow_start
Proof state before:
case hs
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ c ∈ ball c p

case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p
Tactic:
exact mem_ball_self pp
Proof state after:
case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p
Theorem: Super.grow_start
Proof state before:
case ht
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ closedBall 0 (p / 2) ⊆ ball 0 p
Tactic:
apply Metric.closedBall_subset_ball
Proof state after:
case ht.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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ p / 2 < p
Theorem: Super.grow_start
Proof state before:
case ht.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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
⊢ p / 2 < p
Tactic:
exact half_lt_self pp
Proof state after:
no goals
Theorem: Super.grow_start
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ r c 0 = a
Tactic:
convert rb.self_of_nhds
Proof state after:
case h.e'_2.h.e'_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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ 0 = s.bottcherNear (c, a).1 (c, a).2
Theorem: Super.grow_start
Proof state before:
case h.e'_2.h.e'_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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
⊢ 0 = s.bottcherNear (c, a).1 (c, a).2
Tactic:
simp only [s.bottcherNear_a]
Proof state after:
no goals
Theorem: Super.grow_start
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
s : Super f d a
c : ℂ
ba : HolomorphicAt (I.prod I) I (uncurry s.bottcherNear) (c, a)
nc : mfderiv I I (s.bottcherNear c) a ≠ 0
r : ℂ → ℂ → S
ra : HolomorphicAt (I.prod I) I (uncurry r) (c, 0)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), s.bottcherNear x.1 (r x.1 x.2) = x.2
rm : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
t : Set (ℂ × ℂ)
o : IsOpen t
m✝ : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
h :
  ∀ x ∈ ball (c, 0) p,
    HolomorphicAt (I.prod I) I (uncurry r) x ∧ s.bottcherNear x.1 (r x.1 x.2) = x.2 ∧ (x.1, r x.1 x.2) ∈ s.near
nb : ball (c, 0) p ∈ 𝓝ˢ ({c} ×ˢ closedBall 0 (p / 2))
x✝ : ℂ × ℂ
m : x✝ ∈ ball (c, 0) p
⊢ s.bottcherNear x✝.1 ((f x✝.1)^[0] (r x✝.1 x✝.2)) = x✝.2 ^ d ^ 0
Tactic:
simp only [Function.iterate_zero_apply, pow_zero, pow_one, (h _ m).2.1]
Proof state after:
no goals
Theorem: Grow.open
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 : Grow s c p n r
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
have e := g.eqn
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ ({c} ×ˢ closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
simp only [isCompact_singleton.nhdsSet_prod_eq (isCompact_closedBall _ _)] at e
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Theorem: Grow.open
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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases Filter.mem_prod_iff.mp e with ⟨a', an, b', bn, sub⟩
Proof state after:
case 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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : a' ×ˢ b' ⊆ {x | (fun x => Eqn s n r x) x}
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Theorem: Grow.open
Proof state before:
case 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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : a' ×ˢ b' ⊆ {x | (fun x => Eqn s n r x) x}
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
simp only [subset_setOf] at sub
Proof state after:
case 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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Theorem: Grow.open
Proof state before:
case 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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases eventually_nhds_iff.mp (nhdsSet_singleton.subst an) with ⟨a, aa, ao, am⟩
Proof state after:
case intro.intro.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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Theorem: Grow.open
Proof state before:
case intro.intro.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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r
Tactic:
rcases eventually_nhdsSet_iff_exists.mp bn with ⟨b, bo, bp, bb⟩
Proof state after:
case intro.intro.intro.intro.intro.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 : Grow s c p n r
e : ∀ᶠ (x : ℂ × ℂ) in 𝓝ˢ {c} ×ˢ 𝓝ˢ (closedBall 0 p), Eqn s n r x
a' : Set ℂ
an : a' ∈ 𝓝ˢ {c}
b' : Set ℂ
bn : b' ∈ 𝓝ˢ (closedBall 0 p)
sub : ∀ x ∈ a' ×ˢ b', Eqn s n r x
a : Set ℂ
aa : ∀ x ∈ a, a' x
ao : IsOpen a
am : c ∈ a
b : Set ℂ
bo : IsOpen b
bp : closedBall 0 p ⊆ b
bb : ∀ x ∈ b, b' x
⊢ ∃ p', p < p' ∧ ∀ᶠ (c' : ℂ) in 𝓝 c, Grow s c' p' n r