internlm/Lean-Github huggingface dataset:
Theorem: Grow.p1
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
p1 : ¬p < 1
⊢ False
Tactic:
simp only [not_lt] at p1
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
p1 : 1 ≤ p
⊢ False
Theorem: Grow.p1
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
p1 : 1 ≤ p
⊢ False
Tactic:
have e := (g.eqn.filter_mono (nhds_le_nhdsSet (x := (c, 1)) ?_)).self_of_nhds
Proof state after:
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 : Grow s c p n r
p1 : 1 ≤ p
e : Eqn s n r (c, 1)
⊢ False

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 : Grow s c p n r
p1 : 1 ≤ p
⊢ (c, 1) ∈ {c} ×ˢ closedBall 0 p
Theorem: Grow.p1
Proof state before:
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 : Grow s c p n r
p1 : 1 ≤ p
e : Eqn s n r (c, 1)
⊢ False
Tactic:
have lt := s.potential_lt_one ⟨_, e.near⟩
Proof state after:
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 : Grow s c p n r
p1 : 1 ≤ p
e : Eqn s n r (c, 1)
lt : s.potential (c, 1).1 (r (c, 1).1 (c, 1).2) < 1
⊢ False
Theorem: Grow.p1
Proof state before:
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 : Grow s c p n r
p1 : 1 ≤ p
e : Eqn s n r (c, 1)
lt : s.potential (c, 1).1 (r (c, 1).1 (c, 1).2) < 1
⊢ False
Tactic:
rw [e.potential, Complex.abs.map_one, lt_self_iff_false] at lt
Proof state after:
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 : Grow s c p n r
p1 : 1 ≤ p
e : Eqn s n r (c, 1)
lt : False
⊢ False
Theorem: Grow.p1
Proof state before:
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 : Grow s c p n r
p1 : 1 ≤ p
e : Eqn s n r (c, 1)
lt : False
⊢ False
Tactic:
exact lt
Proof state after:
no goals
Theorem: Grow.p1
Proof state before:
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 : Grow s c p n r
p1 : 1 ≤ p
⊢ (c, 1) ∈ {c} ×ˢ closedBall 0 p
Tactic:
simp only [p1, singleton_prod, mem_image, mem_closedBall_zero_iff, Complex.norm_eq_abs,
  Prod.mk.inj_iff, eq_self_iff_true, true_and_iff, exists_eq_right, Complex.abs.map_one]
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 : ℂ
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
have ba := s.bottcherNear_holomorphic _ (s.mem_near c)
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)
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
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)
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
have nc := s.bottcherNear_mfderiv_ne_zero c
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
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
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
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rcases complex_inverse_fun ba nc with ⟨r, ra, rb, br⟩
Proof state after:
case 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
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, s.bottcherNear c a)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNear c a), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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, s.bottcherNear c a)
rb : ∀ᶠ (x : ℂ × S) in 𝓝 (c, a), r x.1 (s.bottcherNear x.1 x.2) = x.2
br : ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, s.bottcherNear c a), s.bottcherNear x.1 (r x.1 x.2) = x.2
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rw [s.bottcherNear_a] at ra br
Proof state after:
case 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
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
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
have rm : ∀ᶠ x : ℂ × ℂ in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near := by
  refine (continuousAt_fst.prod ra.continuousAt).eventually_mem (s.isOpen_near.mem_nhds ?_)
  have r0 := rb.self_of_nhds; simp only [s.bottcherNear_a] at r0
  simp only [uncurry, r0]; exact s.mem_near c
Proof state after:
case 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
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
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rcases eventually_nhds_iff.mp (ra.eventually.and (br.and rm)) with ⟨t, h, o, m⟩
Proof state after:
case 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
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 (ℂ × ℂ)
h : ∀ x ∈ t, 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
o : IsOpen t
m : (c, 0) ∈ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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 (ℂ × ℂ)
h : ∀ x ∈ t, 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
o : IsOpen t
m : (c, 0) ∈ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
rcases Metric.isOpen_iff.mp o _ m with ⟨p, pp, sub⟩
Proof state after:
case 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
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 (ℂ × ℂ)
h : ∀ x ∈ t, 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
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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 (ℂ × ℂ)
h : ∀ x ∈ t, 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
o : IsOpen t
m : (c, 0) ∈ t
p : ℝ
pp : p > 0
sub : ball (c, 0) p ⊆ t
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
replace h := fun (x : ℂ × ℂ) m ↦ h x (sub m)
Proof state after:
case 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
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 r, 0 < p ∧ Grow s c p 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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 r, 0 < p ∧ Grow s c p 0 r
Tactic:
have nb : ball (c, (0 : ℂ)) p ∈ 𝓝ˢ ({c} ×ˢ closedBall (0 : ℂ) (p / 2)) := by
  rw [isOpen_ball.mem_nhdsSet, ← ball_prod_same]; apply prod_mono
  rw [singleton_subset_iff]; exact mem_ball_self pp
  apply Metric.closedBall_subset_ball; exact half_lt_self pp
Proof state after:
case 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
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))
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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))
⊢ ∃ p r, 0 < p ∧ Grow s c p 0 r
Tactic:
use p / 2, r, half_pos pp
Proof state after:
case 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
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))
⊢ Grow s c (p / 2) 0 r
Theorem: Super.grow_start
Proof state before:
case 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
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))
⊢ Grow s c (p / 2) 0 r
Tactic:
exact
  { nonneg := (half_pos pp).le
    zero := by convert rb.self_of_nhds; simp only [s.bottcherNear_a]
    start := Filter.eventually_iff_exists_mem.mpr ⟨_, ball_mem_nhds _ pp, fun _ m ↦ (h _ m).2.1⟩
    eqn :=
      Filter.eventually_iff_exists_mem.mpr
        ⟨_, nb, fun _ m ↦
          { holo := (h _ m).1
            near := (h _ m).2.2
            eqn := by simp only [Function.iterate_zero_apply, pow_zero, pow_one, (h _ m).2.1] }⟩ }
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
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0), (x.1, r x.1 x.2) ∈ s.near
Tactic:
refine (continuousAt_fst.prod ra.continuousAt).eventually_mem (s.isOpen_near.mem_nhds ?_)
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
⊢ ((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
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near
Tactic:
have r0 := rb.self_of_nhds
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, a).1 (s.bottcherNear (c, a).1 (c, a).2) = (c, a).2
⊢ ((c, 0).1, uncurry r (c, 0)) ∈ s.near